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

Theorem impbid 128
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 127 . 2 (𝜑 → (𝜑 → (𝜓𝜒)))
43pm2.43i 49 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bicom1  130  impbid1  141  pm5.74  178  imbi1d  230  pm5.501  243  pm5.32d  445  impbida  585  notbi  655  pm5.21  684  nbn2  686  2falsed  691  pm5.21ndd  694  oibabs  703  orbi2d  779  con4biddc  842  con1bidc  859  con1bdc  863  dedlema  953  dedlemb  954  xorbin  1362  albi  1444  19.21ht  1560  exbi  1583  19.23t  1655  equequ1  1688  equequ2  1689  elequ1  1690  elequ2  1691  equsexd  1707  dral1  1708  cbv2h  1724  sbequ12  1744  sbiedh  1760  drex1  1770  ax11b  1798  sbequ  1812  sbft  1820  sb56  1857  cbvexdh  1898  eupickb  2080  eupickbi  2081  ceqsalt  2712  ceqex  2812  mob2  2864  euxfr2dc  2869  reu6  2873  sbciegft  2939  csbiebt  3039  sseq1  3120  reupick  3360  reupick2  3362  disjeq2  3910  disjeq1  3913  exmidsssnc  4126  copsexg  4166  euotd  4176  poeq2  4222  sotritric  4246  sotritrieq  4247  seeq1  4261  seeq2  4262  alxfr  4382  ralxfrd  4383  rexxfrd  4384  ordelsuc  4421  sosng  4612  iss  4865  iotaval  5099  funeq  5143  funssres  5165  f0dom0  5316  tz6.12c  5451  fnbrfvb  5462  ssimaex  5482  fvimacnv  5535  elpreima  5539  fsn  5592  fconst2g  5635  elunirn  5667  f1ocnvfvb  5681  foeqcnvco  5691  f1eqcocnv  5692  fliftfun  5697  isose  5722  isopo  5724  isoso  5726  f1oiso2  5728  eusvobj2  5760  oprabid  5803  f1opw2  5976  op1steq  6077  rntpos  6154  frecabcl  6296  nnsucelsuc  6387  nnsucsssuc  6388  nnsseleq  6397  nnaord  6405  nnmord  6413  nnaordex  6423  nnawordex  6424  nnm00  6425  erexb  6454  swoord1  6458  swoord2  6459  iinerm  6501  fundmen  6700  mapxpen  6742  ssenen  6745  nneneq  6751  nndomo  6758  fidifsnen  6764  en1eqsnbi  6837  suplub2ti  6888  isoti  6894  ordiso2  6920  ordiso  6921  ctm  6994  ctssdc  6998  enomni  7011  pm54.43  7051  pr2ne  7053  ltexnqq  7228  genprndl  7341  genprndu  7342  nqprl  7371  nqpru  7372  1idprl  7410  1idpru  7411  ltexprlemrnd  7425  ltaprg  7439  recexprlemrnd  7449  cauappcvgprlemrnd  7470  caucvgprlemrnd  7493  caucvgprprlemrnd  7521  suplocexprlemrl  7537  suplocexprlemru  7539  map2psrprg  7625  ltxrlt  7842  lttri3  7856  addlsub  8144  addid0  8147  ltadd2  8193  eqord1  8257  reapti  8353  apreap  8361  ltmul1  8366  apreim  8377  ltleap  8406  mulap0b  8428  apmul1  8560  lt2msq  8656  nnsub  8771  zltnle  9112  zleloe  9113  zrevaddcl  9116  zltp1le  9120  zapne  9137  nn0n0n1ge2b  9142  zdiv  9151  nneo  9166  zeo2  9169  qrevaddcl  9448  npnflt  9610  nmnfgt  9613  xltneg  9631  xleadd1  9670  iccid  9720  zltaddlt1le  9801  fzn  9834  0fz1  9837  uzsplit  9884  fzm1  9892  fzrevral  9897  ssfzo12bi  10014  qltnle  10035  ioo0  10049  ioom  10050  ico0  10051  ioc0  10052  flqge  10067  modqid2  10136  modqmuladd  10151  frec2uzlt2d  10189  shftlem  10600  shftuz  10601  caucvgrelemcau  10764  sqrtsq  10828  abs00ap  10846  cau3lem  10898  maxleb  11000  rexico  11005  negfi  11011  climshft  11085  zsumdc  11165  fsum3  11168  fsum00  11243  dvdsval2  11507  moddvds  11513  negdvdsb  11520  dvdsnegb  11521  dvdscmulr  11533  dvdsmulcr  11534  dvdssub2  11546  fzo0dvdseq  11566  ltoddhalfle  11601  dvdsgcdb  11712  gcdzeq  11721  dvdssqlem  11729  lcmeq0  11763  lcmdvdsb  11776  coprmgcdb  11780  ncoprmgcdne1b  11781  cncongr  11797  isprm2lem  11808  dvdsprime  11814  dvdsprm  11828  coprm  11833  euclemma  11835  rpexp  11842  hashgcdlem  11914  enct  11957  toponcomb  12209  tgss3  12261  isopn3  12308  neiint  12328  neipsm  12337  opnneissb  12338  opnssneib  12339  tpnei  12343  opnneiid  12347  restopnb  12364  tgcn  12391  tgcnp  12392  iscnp4  12401  cnpnei  12402  cnntr  12408  lmss  12429  upxp  12455  txcn  12458  txlm  12462  hmeoopn  12494  hmeocld  12495  xblm  12600  blssexps  12612  blssex  12613  isxms2  12635  neibl  12674  metss  12677  metrest  12689  metcnp3  12694  ivthinclemlr  12798  ivthinclemur  12800  cnplimccntop  12822  eflt  12879  subctctexmid  13280  triap  13310
  Copyright terms: Public domain W3C validator