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

Theorem impbid 127
Description: Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 3-Nov-2012.)
Hypotheses
Ref Expression
impbid.1 (𝜑 → (𝜓𝜒))
impbid.2 (𝜑 → (𝜒𝜓))
Assertion
Ref Expression
impbid (𝜑 → (𝜓𝜒))

Proof of Theorem impbid
StepHypRef Expression
1 impbid.1 . . 3 (𝜑 → (𝜓𝜒))
2 impbid.2 . . 3 (𝜑 → (𝜒𝜓))
31, 2impbid21d 126 . 2 (𝜑 → (𝜑 → (𝜓𝜒)))
43pm2.43i 48 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-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bicom1  129  impbid1  140  pm5.74  177  imbi1d  229  pm5.501  242  pm5.32d  438  impbida  561  notbid  625  pm5.21  644  nbn2  646  2falsed  651  pm5.21ndd  654  orbi2d  737  con4biddc  790  con1bidc  804  con1bdc  808  oibabs  836  dedlema  913  dedlemb  914  xorbin  1318  albi  1400  19.21ht  1516  exbi  1538  19.23t  1610  equequ1  1642  equequ2  1643  elequ1  1644  elequ2  1645  equsexd  1661  dral1  1662  cbv2h  1678  sbequ12  1698  sbiedh  1714  drex1  1723  ax11b  1751  sbequ  1765  sbft  1773  sb56  1810  cbvexdh  1846  eupickb  2026  eupickbi  2027  ceqsalt  2639  ceqex  2735  mob2  2786  euxfr2dc  2791  reu6  2795  sbciegft  2858  csbiebt  2956  sseq1  3036  reupick  3272  reupick2  3274  disjeq2  3805  disjeq1  3808  copsexg  4045  euotd  4055  poeq2  4101  sotritric  4125  sotritrieq  4126  seeq1  4140  seeq2  4141  alxfr  4257  ralxfrd  4258  rexxfrd  4259  ordelsuc  4295  sosng  4479  iss  4725  iotaval  4957  funeq  5000  funssres  5021  f0dom0  5167  tz6.12c  5297  fnbrfvb  5308  ssimaex  5328  fvimacnv  5377  elpreima  5381  fsn  5432  fconst2g  5473  elunirn  5506  f1ocnvfvb  5520  foeqcnvco  5530  f1eqcocnv  5531  fliftfun  5536  isose  5561  isopo  5563  isoso  5565  f1oiso2  5567  eusvobj2  5599  oprabid  5638  f1opw2  5807  op1steq  5906  rntpos  5976  frecabcl  6118  nnsucelsuc  6206  nnsucsssuc  6207  nnsseleq  6216  nnaord  6220  nnmord  6228  nnaordex  6238  nnawordex  6239  nnm00  6240  erexb  6269  swoord1  6273  swoord2  6274  iinerm  6316  fundmen  6475  mapxpen  6516  ssenen  6519  nneneq  6525  nndomo  6532  fidifsnen  6538  en1eqsnbi  6607  suplub2ti  6640  isoti  6646  ordiso2  6672  ordiso  6673  enomni  6739  pm54.43  6762  pr2ne  6764  ltexnqq  6911  genprndl  7024  genprndu  7025  nqprl  7054  nqpru  7055  1idprl  7093  1idpru  7094  ltexprlemrnd  7108  ltaprg  7122  recexprlemrnd  7132  cauappcvgprlemrnd  7153  caucvgprlemrnd  7176  caucvgprprlemrnd  7204  ltxrlt  7496  lttri3  7509  addlsub  7792  addid0  7795  ltadd2  7841  reapti  7997  apreap  8005  ltmul1  8010  apreim  8021  ltleap  8048  mulap0b  8063  apmul1  8194  lt2msq  8282  nnsub  8395  zltnle  8729  zleloe  8730  zrevaddcl  8733  zltp1le  8737  zapne  8754  nn0n0n1ge2b  8759  zdiv  8767  nneo  8782  zeo2  8785  qrevaddcl  9061  xltneg  9230  iccid  9275  zltaddlt1le  9355  fzn  9388  0fz1  9391  uzsplit  9436  fzm1  9444  fzrevral  9449  ssfzo12bi  9564  qltnle  9585  ioo0  9599  ioom  9600  ico0  9601  ioc0  9602  flqge  9617  modqid2  9686  modqmuladd  9701  frec2uzlt2d  9739  shftlem  10147  shftuz  10148  caucvgrelemcau  10309  sqrtsq  10373  abs00ap  10391  cau3lem  10443  maxleb  10545  rexico  10550  negfi  10554  climshft  10587  zisum  10665  fisum  10667  dvdsval2  10681  moddvds  10687  negdvdsb  10694  dvdsnegb  10695  dvdscmulr  10707  dvdsmulcr  10708  dvdssub2  10720  fzo0dvdseq  10740  ltoddhalfle  10775  dvdsgcdb  10884  gcdzeq  10893  dvdssqlem  10901  lcmeq0  10935  lcmdvdsb  10948  coprmgcdb  10952  ncoprmgcdne1b  10953  cncongr  10969  isprm2lem  10980  dvdsprime  10986  dvdsprm  11000  coprm  11005  euclemma  11007  rpexp  11014  hashgcdlem  11085  bj-notbi  11261
  Copyright terms: Public domain W3C validator