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  900  rbaibr  903  rbaibd  908  dedlem0a  950  jaoi2OLD  967  unineq  3748  fvopab6  5975  fressnfv  6076  tpostpos  6976  odi  7229  nnmword  7283  ltmpi  9283  maducoeval2  18949  hausdiag  19973  numclwwlkun  24853  mdbr2  26988  mdsl2i  27014  itg2addnclem  29919  itg2addnclem3  29921  rmydioph  30787  expdioph  30796
  Copyright terms: Public domain W3C validator