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  788  con1bidc  802  con1bdc  806  oibabs  834  dedlema  911  dedlemb  912  xorbin  1316  albi  1398  19.21ht  1514  exbi  1536  19.23t  1608  equequ1  1639  equequ2  1640  elequ1  1641  elequ2  1642  equsexd  1658  dral1  1659  cbv2h  1675  sbequ12  1695  sbiedh  1711  drex1  1720  ax11b  1748  sbequ  1762  sbft  1770  sb56  1807  cbvexdh  1843  eupickb  2023  eupickbi  2024  ceqsalt  2626  ceqex  2723  mob2  2773  euxfr2dc  2778  reu6  2782  sbciegft  2845  csbiebt  2943  sseq1  3021  reupick  3255  reupick2  3257  disjeq2  3778  disjeq1  3781  copsexg  4007  euotd  4017  poeq2  4063  sotritric  4087  sotritrieq  4088  seeq1  4102  seeq2  4103  alxfr  4219  ralxfrd  4220  rexxfrd  4221  ordelsuc  4257  sosng  4439  iss  4684  iotaval  4908  funeq  4951  funssres  4972  tz6.12c  5235  fnbrfvb  5246  ssimaex  5266  fvimacnv  5314  elpreima  5318  fsn  5367  fconst2g  5408  elunirn  5437  f1ocnvfvb  5451  foeqcnvco  5461  f1eqcocnv  5462  fliftfun  5467  isose  5491  isopo  5493  isoso  5495  f1oiso2  5497  eusvobj2  5529  oprabid  5568  f1opw2  5737  op1steq  5836  rntpos  5906  frecabcl  6048  nnsucelsuc  6135  nnsucsssuc  6136  nnsseleq  6145  nnaord  6148  nnmord  6156  nnaordex  6166  nnawordex  6167  nnm00  6168  erexb  6197  swoord1  6201  swoord2  6202  iinerm  6244  fundmen  6353  nneneq  6392  nndomo  6399  fidifsnen  6405  suplub2ti  6473  isoti  6479  ordiso2  6505  ordiso  6506  pm54.43  6518  pr2ne  6520  ltexnqq  6660  genprndl  6773  genprndu  6774  nqprl  6803  nqpru  6804  1idprl  6842  1idpru  6843  ltexprlemrnd  6857  ltaprg  6871  recexprlemrnd  6881  cauappcvgprlemrnd  6902  caucvgprlemrnd  6925  caucvgprprlemrnd  6953  ltxrlt  7245  lttri3  7258  addlsub  7541  addid0  7544  ltadd2  7590  reapti  7746  apreap  7754  ltmul1  7759  apreim  7770  ltleap  7797  mulap0b  7812  apmul1  7943  lt2msq  8031  nnsub  8144  zltnle  8478  zleloe  8479  zrevaddcl  8482  zltp1le  8486  zapne  8503  nn0n0n1ge2b  8508  zdiv  8516  nneo  8531  zeo2  8534  qrevaddcl  8810  xltneg  8979  iccid  9024  zltaddlt1le  9104  fzn  9137  0fz1  9140  uzsplit  9185  fzm1  9193  fzrevral  9198  ssfzo12bi  9311  qltnle  9332  ioo0  9346  ioom  9347  ico0  9348  ioc0  9349  flqge  9364  modqid2  9433  modqmuladd  9448  frec2uzlt2d  9486  shftlem  9842  shftuz  9843  caucvgrelemcau  10004  sqrtsq  10068  abs00ap  10086  cau3lem  10138  maxleb  10240  rexico  10245  negfi  10248  climshft  10281  dvdsval2  10343  moddvds  10349  negdvdsb  10356  dvdsnegb  10357  dvdscmulr  10369  dvdsmulcr  10370  dvdssub2  10382  fzo0dvdseq  10402  ltoddhalfle  10437  dvdsgcdb  10546  gcdzeq  10555  dvdssqlem  10563  lcmeq0  10597  lcmdvdsb  10610  coprmgcdb  10614  ncoprmgcdne1b  10615  cncongr  10631  isprm2lem  10642  dvdsprime  10648  dvdsprm  10662  coprm  10667  euclemma  10669  rpexp  10676  bj-notbi  10874
  Copyright terms: Public domain W3C validator