MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iba Unicode version

Theorem iba 491
Description: Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.)
Assertion
Ref Expression
iba  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )

Proof of Theorem iba
StepHypRef Expression
1 pm3.21 437 . 2  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
2 simpl 445 . 2  |-  ( ( ps  /\  ph )  ->  ps )
31, 2impbid1 196 1  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  biantru  493  biantrud  495  ancrb  535  pm5.54  875  rbaibd  881  dedlem0a  923  unineq  3326  fvopab6  5473  fressnfv  5559  tpostpos  6106  odi  6463  nnmword  6517  ltmpi  8408  hausdiag  17171  mdbr2  22706  mdsl2i  22732  wl-dedlem0a  24096  rmydioph  26273  expdioph  26282
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator