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

Theorem iba 501
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 446 . 2  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
2 simpl 455 . 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 367
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 369
This theorem is referenced by:  biantru  503  biantrud  505  ancrb  548  pm5.54  900  rbaibr  903  rbaibd  908  dedlem0a  950  unineq  3745  fvopab6  5956  fressnfv  6061  tpostpos  6967  odi  7220  nnmword  7274  ltmpi  9271  maducoeval2  19309  hausdiag  20312  numclwwlkun  25281  mdbr2  27413  mdsl2i  27439  itg2addnclem  30306  itg2addnclem3  30308  rmydioph  31195  expdioph  31204
  Copyright terms: Public domain W3C validator