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  7271  pr2ne  7273  ltexnqq  7494  genprndl  7607  genprndu  7608  nqprl  7637  nqpru  7638  1idprl  7676  1idpru  7677  ltexprlemrnd  7691  ltaprg  7705  recexprlemrnd  7715  cauappcvgprlemrnd  7736  caucvgprlemrnd  7759  caucvgprprlemrnd  7787  suplocexprlemrl  7803  suplocexprlemru  7805  map2psrprg  7891  ltxrlt  8111  lttri3  8125  addlsub  8415  addid0  8418  ltadd2  8465  eqord1  8529  reapti  8625  apreap  8633  ltmul1  8638  apreim  8649  ltleap  8678  mulap0b  8701  recapb  8717  apmul1  8834  rerecapb  8889  lt2msq  8932  nnsub  9048  zltnle  9391  zleloe  9392  zrevaddcl  9395  zltp1le  9399  zapne  9419  nn0n0n1ge2b  9424  zdiv  9433  nneo  9448  zeo2  9451  qrevaddcl  9737  npnflt  9909  nmnfgt  9912  xltneg  9930  xleadd1  9969  iccid  10019  zltaddlt1le  10101  fzn  10136  0fz1  10139  uzsplit  10186  fzm1  10194  fzrevral  10199  ssfzo12bi  10320  qltnle  10352  ioo0  10368  ioom  10369  ico0  10370  ioc0  10371  flqge  10391  modqid2  10462  modqmuladd  10477  frec2uzlt2d  10515  seqf1oglem1  10630  qsqeqor  10761  nn0ltexp2  10820  len0nnbi  10988  shftlem  11000  shftuz  11001  caucvgrelemcau  11164  sqrtsq  11228  abs00ap  11246  cau3lem  11298  maxleb  11400  rexico  11405  negfi  11412  climshft  11488  zsumdc  11568  fsum3  11571  fsum00  11646  zproddc  11763  fprodseq  11767  dvdsval2  11974  moddvds  11983  negdvdsb  11991  dvdsnegb  11992  dvdscmulr  12004  dvdsmulcr  12005  dvdssub2  12019  fzo0dvdseq  12041  ltoddhalfle  12077  dvdsgcdb  12207  gcdzeq  12216  dvdssqlem  12224  lcmeq0  12266  lcmdvdsb  12279  coprmgcdb  12283  ncoprmgcdne1b  12284  cncongr  12300  isprm2lem  12311  dvdsprime  12317  dvdsprm  12332  coprm  12339  euclemma  12341  rpexp  12348  prmdiveq  12431  hashgcdlem  12433  odzdvds  12441  pythagtrip  12479  pcdvdsb  12516  pc2dvds  12526  pcprmpw2  12529  pcprmpw  12530  enct  12677  intopsn  13071  gsumfzval  13095  isgrpid2  13244  isgrpinv  13258  f1ghm0to0  13480  ringinvnz1ne0  13683  ringinvnzdiv  13684  unitmulclb  13748  dvreq1  13776  isnzr2  13818  rrgeq0  13899  domneq0  13906  lssats2  14048  lspsneq0  14060  znunit  14293  toponcomb  14372  tgss3  14422  isopn3  14469  neiint  14489  neipsm  14498  opnneissb  14499  opnssneib  14500  tpnei  14504  opnneiid  14508  restopnb  14525  tgcn  14552  tgcnp  14553  iscnp4  14562  cnpnei  14563  cnntr  14569  lmss  14590  upxp  14616  txcn  14619  txlm  14623  hmeoopn  14655  hmeocld  14656  xblm  14761  blssexps  14773  blssex  14774  isxms2  14796  neibl  14835  metss  14838  metrest  14850  metcnp3  14855  ivthinclemlr  14981  ivthinclemur  14983  cnplimccntop  15014  eflt  15119  dvdsppwf1o  15333  lgsdir2lem4  15380  lgsne0  15387  gausslemma2dlem1a  15407  lgsquadlem1  15426  m1lgs  15434  bj-charfunbi  15565  subctctexmid  15755  triap  15786  iswomni0  15808