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

Theorem iba 503
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 448 . 2  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
2 simpl 457 . 2  |-  ( ( ps  /\  ph )  ->  ps )
31, 2impbid1 203 1  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  biantru  505  biantrud  507  ancrb  550  pm5.54  895  rbaibd  901  dedlem0a  943  jaoi2OLD  960  unineq  3612  fvopab6  5808  fressnfv  5908  tpostpos  6777  odi  7030  nnmword  7084  ltmpi  9085  maducoeval2  18458  hausdiag  19230  mdbr2  25712  mdsl2i  25738  itg2addnclem  28455  itg2addnclem3  28457  rmydioph  29375  expdioph  29384  numclwwlkun  30684
  Copyright terms: Public domain W3C validator