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

Theorem biimpd 142
Description: Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
biimpd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimpd (𝜑 → (𝜓𝜒))

Proof of Theorem biimpd
StepHypRef Expression
1 biimpd.1 . 2 (𝜑 → (𝜓𝜒))
2 bi1 116 . 2 ((𝜓𝜒) → (𝜓𝜒))
31, 2syl 14 1 (𝜑 → (𝜓𝜒))
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  4045  euotd  4055  rexxfrd  4259  relop  4554  elres  4715  rnxpid  4831  relcnvtr  4916  iotaval  4957  mpteqb  5356  chfnrn  5373  elpreima  5381  ffnfv  5419  f1elima  5513  f1eqcocnv  5531  fliftfun  5536  isoresbr  5549  isotr  5556  ovmpt2dv2  5735  smoiso  6021  nnaordi  6219  nnaword  6222  nnawordi  6226  xpiderm  6315  iinerm  6316  dom2lem  6441  nneneq  6525  exmidpw  6576  f1dmvrnfibi  6603  pr2nelem  6763  exmidfodomrlemeldju  6769  exmidfodomrlemreseldju  6770  addcanpig  6837  mulcanpig  6838  enqer  6861  ltexnqi  6912  prarloclemlo  6997  genpcdl  7022  genpcuu  7023  appdivnq  7066  ltprordil  7092  1idprl  7093  1idpru  7094  ltexprlemm  7103  ltexprlemopu  7106  ltexprlemru  7115  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  caucvgprprlemopu  7202  caucvgsrlemoffcau  7287  caucvgsrlemoffres  7289  ltrenn  7336  axpre-ltadd  7365  addn0nid  7796  apne  8041  prodgt02  8249  prodge02  8251  mulgt1  8259  divgt0  8268  divge0  8269  cju  8356  nnsub  8395  nominpos  8586  zltnle  8729  nn0n0n1ge2  8750  zdcle  8756  btwnnz  8773  uzm1  8981  supinfneg  9015  infsupneg  9016  ublbneg  9030  cnref1o  9065  ltsubrp  9100  ltaddrp  9101  ge0nemnf  9218  xltnegi  9229  iccsupr  9316  icoshft  9339  iccshftri  9344  iccshftli  9346  iccdili  9348  icccntri  9350  fzdcel  9386  fznlem  9387  fzen  9389  fzofzim  9527  eluzgtdifelfzo  9536  elfzonelfzo  9569  qltnle  9585  addmodlteq  9733  fihashf1rn  10093  cjre  10211  caucvgre  10309  icodiamlt  10508  zisum  10663  dvds2lem  10683  muldvds1  10696  dvdscmulr  10700  dvdsmulcr  10701  dvdsdivcl  10726  oddnn02np1  10755  ndvdsadd  10806  zeqzmulgcd  10837  bezoutlemmain  10862  dfgcd2  10878  gcdmultiple  10884  coprmdvds  10949  divgcdodd  10997  isprm6  11001  prmdvdsexpr  11004  cncongrprm  11011  phiprmpw  11073  ch2var  11106  bj-rspgt  11124  bj-nntrans  11284  bj-nnelirr  11286  bj-omtrans  11289  setindft  11298  bj-inf2vnlem3  11305  bj-inf2vnlem4  11306  bj-findis  11312
  Copyright terms: Public domain W3C validator