MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iba 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  3555  fvopab6  5789  fressnfv  5883  tpostpos  6462  odi  6785  nnmword  6839  ltmpi  8741  hausdiag  17634  mdbr2  23756  mdsl2i  23782  wl-dedlem0a  26140  itg2addnclem  26159  itg2addnclem3  26161  rmydioph  26979  expdioph  26988
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