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 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  4110  disjeq1  4113  exmidsssnc  4340  copsexg  4384  euotd  4395  poeq2  4445  sotritric  4469  sotritrieq  4470  seeq1  4484  seeq2  4485  alxfr  4607  ralxfrd  4608  rexxfrd  4609  ordelsuc  4652  sosng  4848  iss  5109  iotaval  5349  funeq  5397  funssres  5420  f0dom0  5586  tz6.12c  5725  fnbrfvb  5741  ssimaex  5764  fvimacnv  5824  elpreima  5828  fsn  5880  fconst2g  5930  fndmexb  5938  elunirn  5972  f1ocnvfvb  5986  foeqcnvco  5996  f1eqcocnv  5997  fliftfun  6002  isose  6027  isopo  6029  isoso  6031  f1oiso2  6033  eusvobj2  6071  oprabid  6117  f1opw2  6296  op1steq  6413  fvn0elsuppb  6492  rntpos  6528  frecabcl  6670  nnsucelsuc  6764  nnsucsssuc  6765  nnsseleq  6774  nnaord  6782  nnmord  6790  nnaordex  6801  nnawordex  6802  nnm00  6803  erexb  6832  swoord1  6836  swoord2  6837  iinerm  6881  mapsnd  6970  fundmen  7094  dom1o  7116  mapxpen  7148  mapunen  7151  ssenen  7152  nneneq  7158  nndomo  7165  fidifsnen  7172  en1eqsnbi  7266  suplub2ti  7341  isoti  7347  ordiso2  7375  ordiso  7376  ctm  7449  ctssdc  7453  enomni  7479  enmkv  7502  enwomni  7510  pm54.43  7536  pr2ne  7538  ltexnqq  7775  genprndl  7888  genprndu  7889  nqprl  7918  nqpru  7919  1idprl  7957  1idpru  7958  ltexprlemrnd  7972  ltaprg  7986  recexprlemrnd  7996  cauappcvgprlemrnd  8017  caucvgprlemrnd  8040  caucvgprprlemrnd  8068  suplocexprlemrl  8084  suplocexprlemru  8086  map2psrprg  8172  ltxrlt  8391  lttri3  8405  addlsub  8697  addid0  8700  ltadd2  8748  eqord1  8812  reapti  8909  apreap  8917  ltmul1  8922  apreim  8933  ltleap  8962  mulap0b  8985  recapb  9003  apmul1  9120  rerecapb  9175  lt2msq  9218  nnsub  9345  zltnle  9694  zleloe  9695  zrevaddcl  9699  zltp1le  9703  zapne  9723  nn0n0n1ge2b  9729  zdiv  9738  nneo  9753  zeo2  9756  qrevaddcl  10053  npnflt  10227  nmnfgt  10230  xltneg  10248  xleadd1  10287  iccid  10337  zltaddlt1le  10420  fzn  10456  0fz1  10459  uzsplit  10509  fzm1  10517  fzrevral  10522  ssfzo12bi  10653  qltnle  10688  ioo0  10704  ioom  10705  ico0  10706  ioc0  10707  flqge  10729  flapge  10730  modqid2  10801  modqmuladd  10816  frec2uzlt2d  10854  seqf1oglem1  10969  qsqeqor  11100  nn0ltexp2  11161  hashtpg  11313  len0nnbi  11353  ccats1pfxeqbi  11528  reuccatpfxs1  11533  shftlem  11595  shftuz  11596  caucvgrelemcau  11760  sqrtsq  11824  abs00ap  11842  cau3lem  11895  maxleb  11997  rexico  12002  negfi  12009  climshft  12086  zsumdc  12167  fsum3  12170  fsum00  12245  zproddc  12362  fprodseq  12366  dvdsval2  12573  moddvds  12582  negdvdsb  12590  dvdsnegb  12591  dvdscmulr  12603  dvdsmulcr  12604  dvdssub2  12618  fzo0dvdseq  12640  ltoddhalfle  12676  dvdsgcdb  12806  gcdzeq  12815  dvdssqlem  12823  lcmeq0  12865  lcmdvdsb  12878  coprmgcdb  12882  ncoprmgcdne1b  12883  cncongr  12899  isprm2lem  12910  dvdsprime  12916  dvdsprm  12932  coprm  12939  euclemma  12941  rpexp  12948  prmdiveq  13034  hashgcdlem  13036  odzdvds  13044  pythagtrip  13082  pcdvdsb  13119  pc2dvds  13129  pcprmpw2  13132  pcprmpw  13133  enct  13373  intopsn  13736  gzsumfzval  13760  isgrpid2  13894  isgrpinv  13908  f1ghm0to0  14124  ringinvnz1ne0  14403  ringinvnzdiv  14404  unitmulclb  14470  dvreq1  14498  isnzr2  14540  rrgeq0  14622  domneq0  14630  lssats2  14800  lspsneq0  14812  znunit  15043  toponcomb  15178  tgss3  15228  isopn3  15275  neiint  15295  neipsm  15304  opnneissb  15305  opnssneib  15306  tpnei  15310  opnneiid  15314  restopnb  15331  tgcn  15358  tgcnp  15359  iscnp4  15368  cnpnei  15369  cnntr  15375  lmss  15396  upxp  15422  txcn  15425  txlm  15429  hmeoopn  15461  hmeocld  15462  xblm  15567  blssexps  15579  blssex  15580  isxms2  15602  neibl  15641  metss  15644  metrest  15656  metcnp3  15661  ivthinclemlr  15787  ivthinclemur  15789  cnplimccntop  15820  eflt  15925  logdivlt  16046  ppiqeq0  16182  dvdsppwf1o  16184  lgsdir2lem4  16248  lgsne0  16255  gausslemma2dlem1a  16275  lgsquadlem1  16294  m1lgs  16302  uhgr0vb  16423  ausgrusgrben  16507  ushgredgedg  16565  ushgredgedgloop  16567  usgr0vb  16572  loopclwwlkn1b  16758  eupth2lem3lem4fi  16812  lealltlt1  16849  lealltlt2  16850  bj-charfunbi  16935  subctctexmid  17128  stnot  17137  triap  17176  iswomni0  17199  alsralrex  17251