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  3361  fvopab6  5520  fressnfv  5606  tpostpos  6153  odi  6510  nnmword  6564  ltmpi  8461  hausdiag  17266  mdbr2  22801  mdsl2i  22827  wl-dedlem0a  24262  rmydioph  26439  expdioph  26448
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