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

Theorem iba 491
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 437 . 2  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
2 simpl 445 . 2  |-  ( ( ps  /\  ph )  ->  ps )
31, 2impbid1 196 1  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  biantru  493  biantrud  495  ancrb  535  pm5.54  875  rbaibd  881  dedlem0a  923  unineq  3394  fvopab6  5555  fressnfv  5641  tpostpos  6188  odi  6545  nnmword  6599  ltmpi  8496  hausdiag  17302  mdbr2  22837  mdsl2i  22863  wl-dedlem0a  24298  rmydioph  26475  expdioph  26484
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator