Theorem impbid 129

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

Step	Hyp	Ref	Expression
1		impbid.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		impbid.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	1, 2	impbid21d 128	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 49	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bicom1  131  impbid1  142  pm5.74  179  imbi1d  231  pm5.501  244  pm5.32d  450  impbida  600  notbi  672  pm5.21  703  nbn2  705  2falsed  710  pm5.21ndd  713  oibabs  722  orbi2d  798  con4biddc  865  con1bidc  882  con1bdc  886  dedlema  978  dedlemb  979  xorbin  1429  albi  1517  19.21ht  1630  exbi  1653  19.23t  1725  equequ1  1760  equequ2  1761  equsexd  1778  dral1  1779  cbv2h  1797  cbv2w  1799  sbequ12  1820  sbiedh  1836  drex1  1847  ax11b  1875  sbequ  1889  sbft  1897  sb56  1936  cbvexdh  1978  eupickb  2164  eupickbi  2165  elequ1  2209  elequ2  2210  ceqsalt  2842  ceqex  2947  mob2  3000  euxfr2dc  3005  reu6  3009  sbciegft  3076  csbiebt  3181  sseq1  3265  reupick  3509  reupick2  3511  disjeq2  4094  disjeq1  4097  exmidsssnc  4321  copsexg  4365  euotd  4376  poeq2  4426  sotritric  4450  sotritrieq  4451  seeq1  4465  seeq2  4466  alxfr  4587  ralxfrd  4588  rexxfrd  4589  ordelsuc  4632  sosng  4828  iss  5089  iotaval  5329  funeq  5377  funssres  5400  f0dom0  5566  tz6.12c  5705  fnbrfvb  5720  ssimaex  5743  fvimacnv  5798  elpreima  5802  fsn  5854  fconst2g  5904  fndmexb  5912  elunirn  5945  f1ocnvfvb  5959  foeqcnvco  5969  f1eqcocnv  5970  fliftfun  5975  isose  6000  isopo  6002  isoso  6004  f1oiso2  6006  eusvobj2  6044  oprabid  6090  f1opw2  6269  op1steq  6386  fvn0elsuppb  6465  rntpos  6501  frecabcl  6643  nnsucelsuc  6737  nnsucsssuc  6738  nnsseleq  6747  nnaord  6755  nnmord  6763  nnaordex  6774  nnawordex  6775  nnm00  6776  erexb  6805  swoord1  6809  swoord2  6810  iinerm  6854  mapsnd  6936  fundmen  7060  dom1o  7082  mapxpen  7114  mapunen  7117  ssenen  7118  nneneq  7124  nndomo  7131  fidifsnen  7138  en1eqsnbi  7232  suplub2ti  7305  isoti  7311  ordiso2  7339  ordiso  7340  ctm  7413  ctssdc  7417  enomni  7443  enmkv  7466  enwomni  7474  pm54.43  7500  pr2ne  7502  ltexnqq  7739  genprndl  7852  genprndu  7853  nqprl  7882  nqpru  7883  1idprl  7921  1idpru  7922  ltexprlemrnd  7936  ltaprg  7950  recexprlemrnd  7960  cauappcvgprlemrnd  7981  caucvgprlemrnd  8004  caucvgprprlemrnd  8032  suplocexprlemrl  8048  suplocexprlemru  8050  map2psrprg  8136  ltxrlt  8355  lttri3  8369  addlsub  8659  addid0  8662  ltadd2  8710  eqord1  8774  reapti  8870  apreap  8878  ltmul1  8883  apreim  8894  ltleap  8923  mulap0b  8946  recapb  8962  apmul1  9079  rerecapb  9134  lt2msq  9177  nnsub  9293  zltnle  9640  zleloe  9641  zrevaddcl  9645  zltp1le  9649  zapne  9669  nn0n0n1ge2b  9675  zdiv  9684  nneo  9699  zeo2  9702  qrevaddcl  9994  npnflt  10167  nmnfgt  10170  xltneg  10188  xleadd1  10227  iccid  10277  zltaddlt1le  10360  fzn  10396  0fz1  10399  uzsplit  10448  fzm1  10456  fzrevral  10461  ssfzo12bi  10592  qltnle  10627  ioo0  10643  ioom  10644  ico0  10645  ioc0  10646  flqge  10666  modqid2  10737  modqmuladd  10752  frec2uzlt2d  10790  seqf1oglem1  10905  qsqeqor  11036  nn0ltexp2  11096  hashtpg  11244  len0nnbi  11284  ccats1pfxeqbi  11459  reuccatpfxs1  11464  shftlem  11526  shftuz  11527  caucvgrelemcau  11690  sqrtsq  11754  abs00ap  11772  cau3lem  11824  maxleb  11926  rexico  11931  negfi  11938  climshft  12014  zsumdc  12095  fsum3  12098  fsum00  12173  zproddc  12290  fprodseq  12294  dvdsval2  12501  moddvds  12510  negdvdsb  12518  dvdsnegb  12519  dvdscmulr  12531  dvdsmulcr  12532  dvdssub2  12546  fzo0dvdseq  12568  ltoddhalfle  12604  dvdsgcdb  12734  gcdzeq  12743  dvdssqlem  12751  lcmeq0  12793  lcmdvdsb  12806  coprmgcdb  12810  ncoprmgcdne1b  12811  cncongr  12827  isprm2lem  12838  dvdsprime  12844  dvdsprm  12859  coprm  12866  euclemma  12868  rpexp  12875  prmdiveq  12958  hashgcdlem  12960  odzdvds  12968  pythagtrip  13006  pcdvdsb  13043  pc2dvds  13053  pcprmpw2  13056  pcprmpw  13057  enct  13268  intopsn  13630  gsumfzval  13654  isgrpid2  13795  isgrpinv  13809  f1ghm0to0  14025  ringinvnz1ne0  14292  ringinvnzdiv  14293  unitmulclb  14359  dvreq1  14387  isnzr2  14429  rrgeq0  14511  domneq0  14519  lssats2  14688  lspsneq0  14700  znunit  14933  toponcomb  15019  tgss3  15069  isopn3  15116  neiint  15136  neipsm  15145  opnneissb  15146  opnssneib  15147  tpnei  15151  opnneiid  15155  restopnb  15172  tgcn  15199  tgcnp  15200  iscnp4  15209  cnpnei  15210  cnntr  15216  lmss  15237  upxp  15263  txcn  15266  txlm  15270  hmeoopn  15302  hmeocld  15303  xblm  15408  blssexps  15420  blssex  15421  isxms2  15443  neibl  15482  metss  15485  metrest  15497  metcnp3  15502  ivthinclemlr  15628  ivthinclemur  15630  cnplimccntop  15661  eflt  15766  dvdsppwf1o  15983  lgsdir2lem4  16030  lgsne0  16037  gausslemma2dlem1a  16057  lgsquadlem1  16076  m1lgs  16084  uhgr0vb  16205  ausgrusgrben  16289  ushgredgedg  16347  ushgredgedgloop  16349  usgr0vb  16354  loopclwwlkn1b  16540  eupth2lem3lem4fi  16594  bj-charfunbi  16707  subctctexmid  16900  triap  16939  iswomni0  16962