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  596  notbi  667  pm5.21  696  nbn2  698  2falsed  703  pm5.21ndd  706  oibabs  715  orbi2d  791  con4biddc  858  con1bidc  875  con1bdc  879  dedlema  971  dedlemb  972  xorbin  1395  albi  1482  19.21ht  1595  exbi  1618  19.23t  1691  equequ1  1726  equequ2  1727  equsexd  1743  dral1  1744  cbv2h  1762  cbv2w  1764  sbequ12  1785  sbiedh  1801  drex1  1812  ax11b  1840  sbequ  1854  sbft  1862  sb56  1900  cbvexdh  1941  eupickb  2126  eupickbi  2127  elequ1  2171  elequ2  2172  ceqsalt  2789  ceqex  2891  mob2  2944  euxfr2dc  2949  reu6  2953  sbciegft  3020  csbiebt  3124  sseq1  3207  reupick  3448  reupick2  3450  disjeq2  4015  disjeq1  4018  exmidsssnc  4237  copsexg  4278  euotd  4288  poeq2  4336  sotritric  4360  sotritrieq  4361  seeq1  4375  seeq2  4376  alxfr  4497  ralxfrd  4498  rexxfrd  4499  ordelsuc  4542  sosng  4737  iss  4993  iotaval  5231  funeq  5279  funssres  5301  f0dom0  5454  tz6.12c  5591  fnbrfvb  5604  ssimaex  5625  fvimacnv  5680  elpreima  5684  fsn  5737  fconst2g  5780  elunirn  5816  f1ocnvfvb  5830  foeqcnvco  5840  f1eqcocnv  5841  fliftfun  5846  isose  5871  isopo  5873  isoso  5875  f1oiso2  5877  eusvobj2  5911  oprabid  5957  f1opw2  6133  op1steq  6246  rntpos  6324  frecabcl  6466  nnsucelsuc  6558  nnsucsssuc  6559  nnsseleq  6568  nnaord  6576  nnmord  6584  nnaordex  6595  nnawordex  6596  nnm00  6597  erexb  6626  swoord1  6630  swoord2  6631  iinerm  6675  fundmen  6874  mapxpen  6918  ssenen  6921  nneneq  6927  nndomo  6934  fidifsnen  6940  en1eqsnbi  7024  suplub2ti  7076  isoti  7082  ordiso2  7110  ordiso  7111  ctm  7184  ctssdc  7188  enomni  7214  enmkv  7237  enwomni  7245  pm54.43  7269  pr2ne  7271  ltexnqq  7492  genprndl  7605  genprndu  7606  nqprl  7635  nqpru  7636  1idprl  7674  1idpru  7675  ltexprlemrnd  7689  ltaprg  7703  recexprlemrnd  7713  cauappcvgprlemrnd  7734  caucvgprlemrnd  7757  caucvgprprlemrnd  7785  suplocexprlemrl  7801  suplocexprlemru  7803  map2psrprg  7889  ltxrlt  8109  lttri3  8123  addlsub  8413  addid0  8416  ltadd2  8463  eqord1  8527  reapti  8623  apreap  8631  ltmul1  8636  apreim  8647  ltleap  8676  mulap0b  8699  recapb  8715  apmul1  8832  rerecapb  8887  lt2msq  8930  nnsub  9046  zltnle  9389  zleloe  9390  zrevaddcl  9393  zltp1le  9397  zapne  9417  nn0n0n1ge2b  9422  zdiv  9431  nneo  9446  zeo2  9449  qrevaddcl  9735  npnflt  9907  nmnfgt  9910  xltneg  9928  xleadd1  9967  iccid  10017  zltaddlt1le  10099  fzn  10134  0fz1  10137  uzsplit  10184  fzm1  10192  fzrevral  10197  ssfzo12bi  10318  qltnle  10350  ioo0  10366  ioom  10367  ico0  10368  ioc0  10369  flqge  10389  modqid2  10460  modqmuladd  10475  frec2uzlt2d  10513  seqf1oglem1  10628  qsqeqor  10759  nn0ltexp2  10818  len0nnbi  10986  shftlem  10998  shftuz  10999  caucvgrelemcau  11162  sqrtsq  11226  abs00ap  11244  cau3lem  11296  maxleb  11398  rexico  11403  negfi  11410  climshft  11486  zsumdc  11566  fsum3  11569  fsum00  11644  zproddc  11761  fprodseq  11765  dvdsval2  11972  moddvds  11981  negdvdsb  11989  dvdsnegb  11990  dvdscmulr  12002  dvdsmulcr  12003  dvdssub2  12017  fzo0dvdseq  12039  ltoddhalfle  12075  dvdsgcdb  12205  gcdzeq  12214  dvdssqlem  12222  lcmeq0  12264  lcmdvdsb  12277  coprmgcdb  12281  ncoprmgcdne1b  12282  cncongr  12298  isprm2lem  12309  dvdsprime  12315  dvdsprm  12330  coprm  12337  euclemma  12339  rpexp  12346  prmdiveq  12429  hashgcdlem  12431  odzdvds  12439  pythagtrip  12477  pcdvdsb  12514  pc2dvds  12524  pcprmpw2  12527  pcprmpw  12528  enct  12675  intopsn  13069  gsumfzval  13093  isgrpid2  13242  isgrpinv  13256  f1ghm0to0  13478  ringinvnz1ne0  13681  ringinvnzdiv  13682  unitmulclb  13746  dvreq1  13774  isnzr2  13816  rrgeq0  13897  domneq0  13904  lssats2  14046  lspsneq0  14058  znunit  14291  toponcomb  14348  tgss3  14398  isopn3  14445  neiint  14465  neipsm  14474  opnneissb  14475  opnssneib  14476  tpnei  14480  opnneiid  14484  restopnb  14501  tgcn  14528  tgcnp  14529  iscnp4  14538  cnpnei  14539  cnntr  14545  lmss  14566  upxp  14592  txcn  14595  txlm  14599  hmeoopn  14631  hmeocld  14632  xblm  14737  blssexps  14749  blssex  14750  isxms2  14772  neibl  14811  metss  14814  metrest  14826  metcnp3  14831  ivthinclemlr  14957  ivthinclemur  14959  cnplimccntop  14990  eflt  15095  dvdsppwf1o  15309  lgsdir2lem4  15356  lgsne0  15363  gausslemma2dlem1a  15383  lgsquadlem1  15402  m1lgs  15410  bj-charfunbi  15541  subctctexmid  15731  triap  15760  iswomni0  15782