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  3421  fvopab6  5623  fressnfv  5709  tpostpos  6256  odi  6579  nnmword  6633  ltmpi  8530  hausdiag  17341  mdbr2  22878  mdsl2i  22904  wl-dedlem0a  24924  itg2addnclem  24933  itg2addnc  24935  rmydioph  27118  expdioph  27127  funressnfv  28002
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