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

Theorem iba 489
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 435 . 2  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
2 simpl 443 . 2  |-  ( ( ps  /\  ph )  ->  ps )
31, 2impbid1 194 1  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  biantru  491  biantrud  493  ancrb  533  pm5.54  870  rbaibd  876  dedlem0a  918  unineq  3419  fvopab6  5621  fressnfv  5707  tpostpos  6254  odi  6577  nnmword  6631  ltmpi  8528  hausdiag  17339  mdbr2  22876  mdsl2i  22902  wl-dedlem0a  24922  rmydioph  27107  expdioph  27116  funressnfv  27991
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 177  df-an 360
  Copyright terms: Public domain W3C validator