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

Theorem biimpd 132
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 111 . 2
31, 2syl 14 1
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  591  mtbird  597  mtbiri  599  orbi2d  703  pm3.37dc  787  pm5.15dc  1277  exlimd2  1483  exintr  1522  19.9d  1548  19.23t  1564  dral1  1615  spimt  1621  cbvalh  1633  chvar  1637  exdistrfor  1678  sbequi  1717  spv  1737  eqrdav  2036  cleqh  2134  ceqsalg  2576  vtoclf  2601  vtocl2  2603  vtocl3  2604  spcdv  2632  rspcdv  2653  elabgt  2678  sbeqalb  2809  eqrd  2957  copsexg  3972  euotd  3982  rexxfrd  4161  relop  4429  elres  4589  rnxpid  4698  relcnvtr  4783  iotaval  4821  mpteqb  5204  chfnrn  5221  elpreima  5229  ffnfv  5266  f1elima  5355  f1eqcocnv  5374  fliftfun  5379  isoresbr  5392  isotr  5399  ovmpt2dv2  5576  smoiso  5858  nnaordi  6017  nnaword  6020  nnawordi  6024  xpiderm  6113  iinerm  6114  dom2lem  6188  addcanpig  6318  mulcanpig  6319  enqer  6342  ltexnqi  6392  prarloclemlo  6477  genpcdl  6502  genpcuu  6503  appdivnq  6544  ltprordil  6565  1idprl  6566  1idpru  6567  ltexprlemm  6574  ltexprlemopu  6577  ltexprlemru  6586  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  axpre-ltadd  6770  apne  7407  prodgt02  7600  prodge02  7602  mulgt1  7610  divgt0  7619  divge0  7620  cju  7694  nnsub  7733  nominpos  7939  zltnle  8067  nn0n0n1ge2  8087  zdcle  8093  btwnnz  8110  uzm1  8279  ublbneg  8324  cnref1o  8357  ltsubrp  8392  ltaddrp  8393  ge0nemnf  8507  xltnegi  8518  iccsupr  8605  icoshft  8628  iccshftri  8633  iccshftli  8635  iccdili  8637  icccntri  8639  fzdcel  8674  fznlem  8675  fzen  8677  elfzmlbmOLD  8759  fzofzim  8814  eluzgtdifelfzo  8823  elfzonelfzo  8856  cjre  9110  ch2var  9242  bj-rspgt  9260  bj-nntrans  9411  bj-nnelirr  9413  bj-omtrans  9416  setindft  9425  bj-inf2vnlem3  9432  bj-inf2vnlem4  9433  bj-findis  9439
  Copyright terms: Public domain W3C validator