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  3432  fvopab6  5637  fressnfv  5723  tpostpos  6270  odi  6593  nnmword  6647  ltmpi  8544  hausdiag  17355  mdbr2  22892  mdsl2i  22918  wl-dedlem0a  24994  itg2addnclem  25003  itg2addnc  25005  rmydioph  27210  expdioph  27219  funressnfv  28096  jaoi2  28176
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