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

Theorem biimpd 136
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 115 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 14 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  mpbid  139  sylibd  142  sylbid  143  mpbidi  144  syl5ib  147  syl6bi  156  ibi  169  imbi1d  224  biimpa  284  notbid  602  mtbird  608  mtbiri  610  orbi2d  714  pm5.15dc  1296  exlimd2  1502  exintr  1541  19.9d  1567  19.23t  1583  dral1  1634  spimt  1640  cbvalh  1652  chvar  1656  exdistrfor  1697  sbequi  1736  spv  1756  eqrdav  2055  cleqh  2153  ceqsalg  2599  vtoclf  2624  vtocl2  2626  vtocl3  2627  spcdv  2655  rspcdv  2676  elabgt  2707  sbcn1  2833  sbcim1  2834  sbcbi1  2835  sbeqalb  2842  sbcel21v  2850  eqrd  2991  copsexg  4009  euotd  4019  rexxfrd  4223  relop  4514  elres  4674  rnxpid  4783  relcnvtr  4868  iotaval  4906  mpteqb  5289  chfnrn  5306  elpreima  5314  ffnfv  5351  f1elima  5440  f1eqcocnv  5459  fliftfun  5464  isoresbr  5477  isotr  5484  ovmpt2dv2  5662  smoiso  5948  nnaordi  6112  nnaword  6115  nnawordi  6119  xpiderm  6208  iinerm  6209  dom2lem  6283  nneneq  6351  addcanpig  6490  mulcanpig  6491  enqer  6514  ltexnqi  6565  prarloclemlo  6650  genpcdl  6675  genpcuu  6676  appdivnq  6719  ltprordil  6745  1idprl  6746  1idpru  6747  ltexprlemm  6756  ltexprlemopu  6759  ltexprlemru  6768  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprprlemopu  6855  caucvgsrlemoffcau  6940  caucvgsrlemoffres  6942  ltrenn  6989  axpre-ltadd  7018  addn0nid  7444  apne  7688  prodgt02  7894  prodge02  7896  mulgt1  7904  divgt0  7913  divge0  7914  cju  7989  nnsub  8028  nominpos  8219  zltnle  8348  nn0n0n1ge2  8369  zdcle  8375  btwnnz  8392  uzm1  8599  ublbneg  8645  cnref1o  8680  ltsubrp  8715  ltaddrp  8716  ge0nemnf  8838  xltnegi  8849  iccsupr  8936  icoshft  8959  iccshftri  8964  iccshftli  8966  iccdili  8968  icccntri  8970  fzdcel  9006  fznlem  9007  fzen  9009  elfzmlbmOLD  9091  fzofzim  9146  eluzgtdifelfzo  9155  elfzonelfzo  9188  qltnle  9203  addmodlteq  9348  cjre  9710  caucvgre  9808  icodiamlt  10007  dvds2lem  10120  muldvds1  10132  dvdscmulr  10136  dvdsmulcr  10137  dvdsdivcl  10162  oddnn02np1  10192  ndvdsadd  10243  ch2var  10294  bj-rspgt  10312  bj-nntrans  10463  bj-nnelirr  10465  bj-omtrans  10468  setindft  10477  bj-inf2vnlem3  10484  bj-inf2vnlem4  10485  bj-findis  10491
  Copyright terms: Public domain W3C validator