ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpar Unicode version

Theorem biimpar 291
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimpar  |-  ( (
ph  /\  ch )  ->  ps )

Proof of Theorem biimpar
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprd 156 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
32imp 122 1  |-  ( (
ph  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  exbiri  374  bitr  456  eqtr  2100  opabss  3863  euotd  4038  wetriext  4348  sosng  4460  xpsspw  4499  brcogw  4553  funimaexglem  5034  funfni  5051  fnco  5059  fnssres  5064  fn0  5070  fnimadisj  5071  fnimaeq0  5072  foco  5168  foimacnv  5196  fvelimab  5282  fvopab3ig  5299  dff3im  5365  dffo4  5368  fmptco  5383  f1eqcocnv  5483  f1ocnv2d  5756  fnexALT  5792  xp1st  5844  xp2nd  5845  tfrlemiubacc  6000  tfri2d  6006  tfr1onlemubacc  6016  tfrcllemubacc  6029  tfri3  6037  ecelqsg  6247  elqsn0m  6262  fidifsnen  6427  recclnq  6680  nq0a0  6745  qreccl  8844  difelfzle  9258  exfzdc  9362  modifeq2int  9504  frec2uzlt2d  9522  1elfz0hash  9866  caucvgrelemcau  10051  recvalap  10168  fzomaxdiflem  10183  divconjdvds  10441  ndvdssub  10521  zsupcllemstep  10532  rplpwr  10607  dvdssqlem  10610  eucialgcvga  10631  mulgcddvds  10667  isprm2lem  10689
  Copyright terms: Public domain W3C validator