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

Theorem iba 490
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 436 . 2  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
2 simpl 444 . 2  |-  ( ( ps  /\  ph )  ->  ps )
31, 2impbid1 195 1  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  biantru  492  biantrud  494  ancrb  534  pm5.54  871  rbaibd  877  dedlem0a  919  jaoi2  934  unineq  3583  fvopab6  5818  fressnfv  5912  tpostpos  6491  odi  6814  nnmword  6868  ltmpi  8773  hausdiag  17669  mdbr2  23791  mdsl2i  23817  wl-dedlem0a  26224  itg2addnclem  26246  itg2addnclem3  26248  rmydioph  27076  expdioph  27085
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator