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  3527  fvopab6  5758  fressnfv  5852  tpostpos  6428  odi  6751  nnmword  6805  ltmpi  8707  hausdiag  17591  mdbr2  23640  mdsl2i  23666  wl-dedlem0a  25939  itg2addnclem  25950  itg2addnc  25952  rmydioph  26769  expdioph  26778
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