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

Theorem iba 490
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 436 . 2  |-  ( ph  ->  ( ps  ->  ( ps  /\  ph ) ) )
2 simpl 444 . 2  |-  ( ( ps  /\  ph )  ->  ps )
31, 2impbid1 195 1  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  biantru  492  biantrud  494  ancrb  534  pm5.54  871  rbaibd  877  dedlem0a  919  jaoi2  934  unineq  3534  fvopab6  5765  fressnfv  5859  tpostpos  6435  odi  6758  nnmword  6812  ltmpi  8714  hausdiag  17598  mdbr2  23647  mdsl2i  23673  wl-dedlem0a  25946  itg2addnclem  25957  itg2addnc  25959  rmydioph  26776  expdioph  26785
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator