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

Theorem biimpd 142
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 116 . 2  |-  ( ( ps  <->  ch )  ->  ( ps  ->  ch ) )
31, 2syl 14 1  |-  ( ph  ->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpbid  145  sylibd  147  sylbid  148  mpbidi  149  syl5ib  152  syl6bi  161  ibi  174  imbi1d  229  biimpa  290  notbid  625  mtbird  631  mtbiri  633  orbi2d  737  pm5.15dc  1323  exlimd2  1529  exintr  1568  19.9d  1594  19.23t  1610  dral1  1662  spimt  1668  cbvalh  1680  chvar  1684  exdistrfor  1725  sbequi  1764  spv  1785  eqrdav  2084  cleqh  2184  ceqsalg  2641  vtoclf  2666  vtocl2  2668  vtocl3  2669  spcdv  2697  rspcdv  2718  elabgt  2748  sbcn1  2875  sbcim1  2876  sbcbi1  2877  sbeqalb  2884  sbcel21v  2892  eqrd  3032  copsexg  4047  euotd  4057  rexxfrd  4261  relop  4556  elres  4717  rnxpid  4833  relcnvtr  4918  iotaval  4959  mpteqb  5358  chfnrn  5375  elpreima  5383  ffnfv  5421  f1elima  5515  f1eqcocnv  5533  fliftfun  5538  isoresbr  5551  isotr  5558  ovmpt2dv2  5737  smoiso  6023  nnaordi  6221  nnaword  6224  nnawordi  6228  xpiderm  6317  iinerm  6318  dom2lem  6443  nneneq  6527  exmidpw  6578  f1dmvrnfibi  6606  pr2nelem  6766  exmidfodomrlemeldju  6772  exmidfodomrlemreseldju  6773  addcanpig  6840  mulcanpig  6841  enqer  6864  ltexnqi  6915  prarloclemlo  7000  genpcdl  7025  genpcuu  7026  appdivnq  7069  ltprordil  7095  1idprl  7096  1idpru  7097  ltexprlemm  7106  ltexprlemopu  7109  ltexprlemru  7118  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  caucvgprprlemopu  7205  caucvgsrlemoffcau  7290  caucvgsrlemoffres  7292  ltrenn  7339  axpre-ltadd  7368  addn0nid  7799  apne  8044  prodgt02  8252  prodge02  8254  mulgt1  8262  divgt0  8271  divge0  8272  cju  8359  nnsub  8398  nominpos  8589  zltnle  8732  nn0n0n1ge2  8753  zdcle  8759  btwnnz  8776  uzm1  8984  supinfneg  9018  infsupneg  9019  ublbneg  9033  cnref1o  9068  ltsubrp  9103  ltaddrp  9104  ge0nemnf  9221  xltnegi  9232  iccsupr  9319  icoshft  9342  iccshftri  9347  iccshftli  9349  iccdili  9351  icccntri  9353  fzdcel  9389  fznlem  9390  fzen  9392  fzofzim  9530  eluzgtdifelfzo  9539  elfzonelfzo  9572  qltnle  9588  addmodlteq  9736  fihashf1rn  10097  cjre  10215  caucvgre  10313  icodiamlt  10512  zisum  10668  dvds2lem  10714  muldvds1  10727  dvdscmulr  10731  dvdsmulcr  10732  dvdsdivcl  10757  oddnn02np1  10786  ndvdsadd  10837  zeqzmulgcd  10868  bezoutlemmain  10893  dfgcd2  10909  gcdmultiple  10915  coprmdvds  10980  divgcdodd  11028  isprm6  11032  prmdvdsexpr  11035  cncongrprm  11042  phiprmpw  11104  ch2var  11137  bj-rspgt  11155  bj-nntrans  11315  bj-nnelirr  11317  bj-omtrans  11320  setindft  11329  bj-inf2vnlem3  11336  bj-inf2vnlem4  11337  bj-findis  11343
  Copyright terms: Public domain W3C validator