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

Theorem biimpd 143
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 117 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 14 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpbid  146  sylibd  148  sylbid  149  mpbidi  150  syl5ib  153  syl6bi  162  ibi  175  imbi1d  230  biimpa  292  mtbird  645  mtbiri  647  orbi2d  762  pm5.15dc  1350  exlimd2  1557  exintr  1596  19.9d  1622  19.23t  1638  dral1  1691  spimt  1697  cbvalh  1709  chvar  1713  exdistrfor  1754  sbequi  1793  spv  1814  eqrdav  2114  cleqh  2215  ceqsalg  2686  vtoclf  2711  vtocl2  2713  vtocl3  2714  spcdv  2743  rspcdv  2764  elabgt  2797  sbcn1  2926  sbcim1  2927  sbcbi1  2928  sbeqalb  2935  sbcel21v  2943  eqrd  3083  exmidsssn  4093  exmidsssnc  4094  copsexg  4134  euotd  4144  rexxfrd  4352  relop  4657  elres  4823  rnxpid  4941  relcnvtr  5026  iotaval  5067  mpteqb  5477  elfvmptrab  5482  chfnrn  5497  elpreima  5505  ffnfv  5544  f1elima  5640  f1eqcocnv  5658  fliftfun  5663  isoresbr  5676  isotr  5683  ovmpodv2  5870  smoiso  6165  nnaordi  6370  nnaword  6373  nnawordi  6377  xpider  6466  iinerm  6467  mptelixpg  6594  dom2lem  6632  nneneq  6717  exmidpw  6768  f1dmvrnfibi  6798  ismkvnex  6995  pr2nelem  7013  exmidfodomrlemeldju  7019  exmidfodomrlemreseldju  7020  addcanpig  7106  mulcanpig  7107  enqer  7130  ltexnqi  7181  prarloclemlo  7266  genpcdl  7291  genpcuu  7292  appdivnq  7335  ltprordil  7361  1idprl  7362  1idpru  7363  ltexprlemm  7372  ltexprlemopu  7375  ltexprlemru  7384  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  caucvgprprlemopu  7471  caucvgsrlemoffcau  7570  caucvgsrlemoffres  7572  ltrenn  7627  axpre-ltadd  7658  addn0nid  8100  apne  8348  prodgt02  8571  prodge02  8573  mulgt1  8581  divgt0  8590  divge0  8591  cju  8679  nnsub  8719  nominpos  8911  zltnle  9054  nn0n0n1ge2  9075  zdcle  9081  btwnnz  9099  uzm1  9308  supinfneg  9342  infsupneg  9343  ublbneg  9357  cnref1o  9392  ltsubrp  9429  ltaddrp  9430  npnflt  9549  nmnfgt  9552  ge0nemnf  9558  xltnegi  9569  xnn0xadd0  9601  iccsupr  9700  icoshft  9724  iccshftri  9729  iccshftli  9731  iccdili  9733  icccntri  9735  fzdcel  9771  fznlem  9772  fzen  9774  fzofzim  9916  eluzgtdifelfzo  9925  elfzonelfzo  9958  qltnle  9974  addmodlteq  10122  fihashf1rn  10486  cjre  10605  caucvgre  10704  icodiamlt  10903  zsumdc  11104  reeff1  11317  dvds2lem  11412  muldvds1  11425  dvdscmulr  11429  dvdsmulcr  11430  dvdsdivcl  11455  oddnn02np1  11484  ndvdsadd  11535  zeqzmulgcd  11566  bezoutlemmain  11593  dfgcd2  11609  gcdmultiple  11615  coprmdvds  11680  divgcdodd  11728  isprm6  11732  prmdvdsexpr  11735  cncongrprm  11742  phiprmpw  11804  lmss  12321  cnplimcim  12711  dvcn  12739  ch2var  12808  bj-rspgt  12827  bj-nntrans  12983  bj-nnelirr  12985  bj-omtrans  12988  setindft  12997  bj-inf2vnlem3  13004  bj-inf2vnlem4  13005  bj-findis  13011
  Copyright terms: Public domain W3C validator