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  454  impbida  604  notbi  676  pm5.21  707  nbn2  709  2falsed  714  pm5.21ndd  717  oibabs  726  orbi2d  802  con4biddc  869  con1bidc  886  con1bdc  890  dedlema  982  dedlemb  983  xorbin  1433  albi  1521  19.21ht  1634  exbi  1657  19.23t  1729  equequ1  1764  equequ2  1765  equsexd  1782  dral1  1783  cbv2h  1801  cbv2w  1803  sbequ12  1824  sbiedh  1840  drex1  1851  ax11b  1879  sbequ  1893  sbft  1901  sb56  1940  cbvexdh  1982  eupickb  2168  eupickbi  2169  elequ1  2213  elequ2  2214  ceqsalt  2848  ceqex  2953  mob2  3006  euxfr2dc  3011  reu6  3015  sbciegft  3082  csbiebt  3187  sseq1  3271  reupick  3517  reupick2  3519  disjeq2  4105  disjeq1  4108  exmidsssnc  4335  copsexg  4379  euotd  4390  poeq2  4440  sotritric  4464  sotritrieq  4465  seeq1  4479  seeq2  4480  alxfr  4602  ralxfrd  4603  rexxfrd  4604  ordelsuc  4647  sosng  4843  iss  5104  iotaval  5344  funeq  5392  funssres  5415  f0dom0  5581  tz6.12c  5720  fnbrfvb  5735  ssimaex  5758  fvimacnv  5815  elpreima  5819  fsn  5871  fconst2g  5921  fndmexb  5929  elunirn  5962  f1ocnvfvb  5976  foeqcnvco  5986  f1eqcocnv  5987  fliftfun  5992  isose  6017  isopo  6019  isoso  6021  f1oiso2  6023  eusvobj2  6061  oprabid  6107  f1opw2  6286  op1steq  6403  fvn0elsuppb  6482  rntpos  6518  frecabcl  6660  nnsucelsuc  6754  nnsucsssuc  6755  nnsseleq  6764  nnaord  6772  nnmord  6780  nnaordex  6791  nnawordex  6792  nnm00  6793  erexb  6822  swoord1  6826  swoord2  6827  iinerm  6871  mapsnd  6960  fundmen  7084  dom1o  7106  mapxpen  7138  mapunen  7141  ssenen  7142  nneneq  7148  nndomo  7155  fidifsnen  7162  en1eqsnbi  7256  suplub2ti  7331  isoti  7337  ordiso2  7365  ordiso  7366  ctm  7439  ctssdc  7443  enomni  7469  enmkv  7492  enwomni  7500  pm54.43  7526  pr2ne  7528  ltexnqq  7765  genprndl  7878  genprndu  7879  nqprl  7908  nqpru  7909  1idprl  7947  1idpru  7948  ltexprlemrnd  7962  ltaprg  7976  recexprlemrnd  7986  cauappcvgprlemrnd  8007  caucvgprlemrnd  8030  caucvgprprlemrnd  8058  suplocexprlemrl  8074  suplocexprlemru  8076  map2psrprg  8162  ltxrlt  8381  lttri3  8395  addlsub  8686  addid0  8689  ltadd2  8737  eqord1  8801  reapti  8897  apreap  8905  ltmul1  8910  apreim  8921  ltleap  8950  mulap0b  8973  recapb  8991  apmul1  9108  rerecapb  9163  lt2msq  9206  nnsub  9322  zltnle  9669  zleloe  9670  zrevaddcl  9674  zltp1le  9678  zapne  9698  nn0n0n1ge2b  9704  zdiv  9713  nneo  9728  zeo2  9731  qrevaddcl  10023  npnflt  10196  nmnfgt  10199  xltneg  10217  xleadd1  10256  iccid  10306  zltaddlt1le  10389  fzn  10425  0fz1  10428  uzsplit  10477  fzm1  10485  fzrevral  10490  ssfzo12bi  10621  qltnle  10656  ioo0  10672  ioom  10673  ico0  10674  ioc0  10675  flqge  10695  modqid2  10766  modqmuladd  10781  frec2uzlt2d  10819  seqf1oglem1  10934  qsqeqor  11065  nn0ltexp2  11125  hashtpg  11277  len0nnbi  11317  ccats1pfxeqbi  11492  reuccatpfxs1  11497  shftlem  11559  shftuz  11560  caucvgrelemcau  11724  sqrtsq  11788  abs00ap  11806  cau3lem  11858  maxleb  11960  rexico  11965  negfi  11972  climshft  12048  zsumdc  12129  fsum3  12132  fsum00  12207  zproddc  12324  fprodseq  12328  dvdsval2  12535  moddvds  12544  negdvdsb  12552  dvdsnegb  12553  dvdscmulr  12565  dvdsmulcr  12566  dvdssub2  12580  fzo0dvdseq  12602  ltoddhalfle  12638  dvdsgcdb  12768  gcdzeq  12777  dvdssqlem  12785  lcmeq0  12827  lcmdvdsb  12840  coprmgcdb  12844  ncoprmgcdne1b  12845  cncongr  12861  isprm2lem  12872  dvdsprime  12878  dvdsprm  12893  coprm  12900  euclemma  12902  rpexp  12909  prmdiveq  12992  hashgcdlem  12994  odzdvds  13002  pythagtrip  13040  pcdvdsb  13077  pc2dvds  13087  pcprmpw2  13090  pcprmpw  13091  enct  13302  intopsn  13664  gzsumfzval  13688  isgrpid2  13822  isgrpinv  13836  f1ghm0to0  14052  ringinvnz1ne0  14327  ringinvnzdiv  14328  unitmulclb  14394  dvreq1  14422  isnzr2  14464  rrgeq0  14546  domneq0  14554  lssats2  14723  lspsneq0  14735  znunit  14966  toponcomb  15052  tgss3  15102  isopn3  15149  neiint  15169  neipsm  15178  opnneissb  15179  opnssneib  15180  tpnei  15184  opnneiid  15188  restopnb  15205  tgcn  15232  tgcnp  15233  iscnp4  15242  cnpnei  15243  cnntr  15249  lmss  15270  upxp  15296  txcn  15299  txlm  15303  hmeoopn  15335  hmeocld  15336  xblm  15441  blssexps  15453  blssex  15454  isxms2  15476  neibl  15515  metss  15518  metrest  15530  metcnp3  15535  ivthinclemlr  15661  ivthinclemur  15663  cnplimccntop  15694  eflt  15799  dvdsppwf1o  16017  lgsdir2lem4  16064  lgsne0  16071  gausslemma2dlem1a  16091  lgsquadlem1  16110  m1lgs  16118  uhgr0vb  16239  ausgrusgrben  16323  ushgredgedg  16381  ushgredgedgloop  16383  usgr0vb  16388  loopclwwlkn1b  16574  eupth2lem3lem4fi  16628  lealltlt1  16665  lealltlt2  16666  bj-charfunbi  16751  subctctexmid  16944  triap  16983  iswomni0  17006