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

Theorem biimpd 132
Description: Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biimpd.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimpd  |-  ( ph  ->  ( ps  ->  ch ) )

Proof of Theorem biimpd
StepHypRef Expression
1 biimpd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 bi1 111 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 14 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpbid  135  sylibd  138  sylbid  139  mpbidi  140  syl5ib  143  syl6bi  152  ibi  165  imbi1d  220  biimpa  280  notbid  592  mtbird  598  mtbiri  600  orbi2d  704  pm3.37dc  788  pm5.15dc  1280  exlimd2  1486  exintr  1525  19.9d  1551  19.23t  1567  dral1  1618  spimt  1624  cbvalh  1636  chvar  1640  exdistrfor  1681  sbequi  1720  spv  1740  eqrdav  2039  cleqh  2137  ceqsalg  2582  vtoclf  2607  vtocl2  2609  vtocl3  2610  spcdv  2638  rspcdv  2659  elabgt  2684  sbeqalb  2815  eqrd  2963  copsexg  3981  euotd  3991  rexxfrd  4195  relop  4486  elres  4646  rnxpid  4755  relcnvtr  4840  iotaval  4878  mpteqb  5261  chfnrn  5278  elpreima  5286  ffnfv  5323  f1elima  5412  f1eqcocnv  5431  fliftfun  5436  isoresbr  5449  isotr  5456  ovmpt2dv2  5634  smoiso  5917  nnaordi  6081  nnaword  6084  nnawordi  6088  xpiderm  6177  iinerm  6178  dom2lem  6252  nneneq  6320  addcanpig  6430  mulcanpig  6431  enqer  6454  ltexnqi  6505  prarloclemlo  6590  genpcdl  6615  genpcuu  6616  appdivnq  6659  ltprordil  6685  1idprl  6686  1idpru  6687  ltexprlemm  6696  ltexprlemopu  6699  ltexprlemru  6708  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  caucvgprprlemopu  6795  caucvgsrlemoffcau  6880  caucvgsrlemoffres  6882  ltrenn  6929  axpre-ltadd  6958  apne  7612  prodgt02  7817  prodge02  7819  mulgt1  7827  divgt0  7836  divge0  7837  cju  7911  nnsub  7950  nominpos  8160  zltnle  8289  nn0n0n1ge2  8309  zdcle  8315  btwnnz  8332  uzm1  8501  ublbneg  8546  cnref1o  8580  ltsubrp  8615  ltaddrp  8616  ge0nemnf  8735  xltnegi  8746  iccsupr  8833  icoshft  8856  iccshftri  8861  iccshftli  8863  iccdili  8865  icccntri  8867  fzdcel  8902  fznlem  8903  fzen  8905  elfzmlbmOLD  8987  fzofzim  9042  eluzgtdifelfzo  9051  elfzonelfzo  9084  qltnle  9099  cjre  9456  caucvgre  9554  icodiamlt  9750  ch2var  9881  bj-rspgt  9899  bj-nntrans  10050  bj-nnelirr  10052  bj-omtrans  10055  setindft  10064  bj-inf2vnlem3  10071  bj-inf2vnlem4  10072  bj-findis  10078
  Copyright terms: Public domain W3C validator