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  598  notbi  670  pm5.21  700  nbn2  702  2falsed  707  pm5.21ndd  710  oibabs  719  orbi2d  795  con4biddc  862  con1bidc  879  con1bdc  883  dedlema  975  dedlemb  976  xorbin  1426  albi  1514  19.21ht  1627  exbi  1650  19.23t  1723  equequ1  1758  equequ2  1759  equsexd  1775  dral1  1776  cbv2h  1794  cbv2w  1796  sbequ12  1817  sbiedh  1833  drex1  1844  ax11b  1872  sbequ  1886  sbft  1894  sb56  1932  cbvexdh  1973  eupickb  2159  eupickbi  2160  elequ1  2204  elequ2  2205  ceqsalt  2827  ceqex  2931  mob2  2984  euxfr2dc  2989  reu6  2993  sbciegft  3060  csbiebt  3165  sseq1  3248  reupick  3489  reupick2  3491  disjeq2  4066  disjeq1  4069  exmidsssnc  4291  copsexg  4334  euotd  4345  poeq2  4395  sotritric  4419  sotritrieq  4420  seeq1  4434  seeq2  4435  alxfr  4556  ralxfrd  4557  rexxfrd  4558  ordelsuc  4601  sosng  4797  iss  5057  iotaval  5296  funeq  5344  funssres  5366  f0dom0  5527  tz6.12c  5665  fnbrfvb  5680  ssimaex  5703  fvimacnv  5758  elpreima  5762  fsn  5815  fconst2g  5864  elunirn  5902  f1ocnvfvb  5916  foeqcnvco  5926  f1eqcocnv  5927  fliftfun  5932  isose  5957  isopo  5959  isoso  5961  f1oiso2  5963  eusvobj2  5999  oprabid  6045  f1opw2  6224  op1steq  6337  rntpos  6418  frecabcl  6560  nnsucelsuc  6654  nnsucsssuc  6655  nnsseleq  6664  nnaord  6672  nnmord  6680  nnaordex  6691  nnawordex  6692  nnm00  6693  erexb  6722  swoord1  6726  swoord2  6727  iinerm  6771  fundmen  6976  dom1o  6997  mapxpen  7029  ssenen  7032  nneneq  7038  nndomo  7045  fidifsnen  7052  en1eqsnbi  7139  suplub2ti  7191  isoti  7197  ordiso2  7225  ordiso  7226  ctm  7299  ctssdc  7303  enomni  7329  enmkv  7352  enwomni  7360  pm54.43  7386  pr2ne  7388  ltexnqq  7618  genprndl  7731  genprndu  7732  nqprl  7761  nqpru  7762  1idprl  7800  1idpru  7801  ltexprlemrnd  7815  ltaprg  7829  recexprlemrnd  7839  cauappcvgprlemrnd  7860  caucvgprlemrnd  7883  caucvgprprlemrnd  7911  suplocexprlemrl  7927  suplocexprlemru  7929  map2psrprg  8015  ltxrlt  8235  lttri3  8249  addlsub  8539  addid0  8542  ltadd2  8589  eqord1  8653  reapti  8749  apreap  8757  ltmul1  8762  apreim  8773  ltleap  8802  mulap0b  8825  recapb  8841  apmul1  8958  rerecapb  9013  lt2msq  9056  nnsub  9172  zltnle  9515  zleloe  9516  zrevaddcl  9520  zltp1le  9524  zapne  9544  nn0n0n1ge2b  9549  zdiv  9558  nneo  9573  zeo2  9576  qrevaddcl  9868  npnflt  10040  nmnfgt  10043  xltneg  10061  xleadd1  10100  iccid  10150  zltaddlt1le  10232  fzn  10267  0fz1  10270  uzsplit  10317  fzm1  10325  fzrevral  10330  ssfzo12bi  10460  qltnle  10493  ioo0  10509  ioom  10510  ico0  10511  ioc0  10512  flqge  10532  modqid2  10603  modqmuladd  10618  frec2uzlt2d  10656  seqf1oglem1  10771  qsqeqor  10902  nn0ltexp2  10961  len0nnbi  11138  ccats1pfxeqbi  11313  reuccatpfxs1  11318  shftlem  11367  shftuz  11368  caucvgrelemcau  11531  sqrtsq  11595  abs00ap  11613  cau3lem  11665  maxleb  11767  rexico  11772  negfi  11779  climshft  11855  zsumdc  11935  fsum3  11938  fsum00  12013  zproddc  12130  fprodseq  12134  dvdsval2  12341  moddvds  12350  negdvdsb  12358  dvdsnegb  12359  dvdscmulr  12371  dvdsmulcr  12372  dvdssub2  12386  fzo0dvdseq  12408  ltoddhalfle  12444  dvdsgcdb  12574  gcdzeq  12583  dvdssqlem  12591  lcmeq0  12633  lcmdvdsb  12646  coprmgcdb  12650  ncoprmgcdne1b  12651  cncongr  12667  isprm2lem  12678  dvdsprime  12684  dvdsprm  12699  coprm  12706  euclemma  12708  rpexp  12715  prmdiveq  12798  hashgcdlem  12800  odzdvds  12808  pythagtrip  12846  pcdvdsb  12883  pc2dvds  12893  pcprmpw2  12896  pcprmpw  12897  enct  13044  intopsn  13440  gsumfzval  13464  isgrpid2  13613  isgrpinv  13627  f1ghm0to0  13849  ringinvnz1ne0  14052  ringinvnzdiv  14053  unitmulclb  14118  dvreq1  14146  isnzr2  14188  rrgeq0  14269  domneq0  14276  lssats2  14418  lspsneq0  14430  znunit  14663  toponcomb  14742  tgss3  14792  isopn3  14839  neiint  14859  neipsm  14868  opnneissb  14869  opnssneib  14870  tpnei  14874  opnneiid  14878  restopnb  14895  tgcn  14922  tgcnp  14923  iscnp4  14932  cnpnei  14933  cnntr  14939  lmss  14960  upxp  14986  txcn  14989  txlm  14993  hmeoopn  15025  hmeocld  15026  xblm  15131  blssexps  15143  blssex  15144  isxms2  15166  neibl  15205  metss  15208  metrest  15220  metcnp3  15225  ivthinclemlr  15351  ivthinclemur  15353  cnplimccntop  15384  eflt  15489  dvdsppwf1o  15703  lgsdir2lem4  15750  lgsne0  15757  gausslemma2dlem1a  15777  lgsquadlem1  15796  m1lgs  15804  uhgr0vb  15925  ausgrusgrben  16007  ushgredgedg  16065  ushgredgedgloop  16067  usgr0vb  16072  loopclwwlkn1b  16214  bj-charfunbi  16342  subctctexmid  16537  triap  16569  iswomni0  16591