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  668  pm5.21  697  nbn2  699  2falsed  704  pm5.21ndd  707  oibabs  716  orbi2d  792  con4biddc  859  con1bidc  876  con1bdc  880  dedlema  972  dedlemb  973  xorbin  1404  albi  1492  19.21ht  1605  exbi  1628  19.23t  1701  equequ1  1736  equequ2  1737  equsexd  1753  dral1  1754  cbv2h  1772  cbv2w  1774  sbequ12  1795  sbiedh  1811  drex1  1822  ax11b  1850  sbequ  1864  sbft  1872  sb56  1910  cbvexdh  1951  eupickb  2137  eupickbi  2138  elequ1  2182  elequ2  2183  ceqsalt  2803  ceqex  2907  mob2  2960  euxfr2dc  2965  reu6  2969  sbciegft  3036  csbiebt  3141  sseq1  3224  reupick  3465  reupick2  3467  disjeq2  4039  disjeq1  4042  exmidsssnc  4263  copsexg  4306  euotd  4317  poeq2  4365  sotritric  4389  sotritrieq  4390  seeq1  4404  seeq2  4405  alxfr  4526  ralxfrd  4527  rexxfrd  4528  ordelsuc  4571  sosng  4766  iss  5024  iotaval  5262  funeq  5310  funssres  5332  f0dom0  5491  tz6.12c  5629  fnbrfvb  5642  ssimaex  5663  fvimacnv  5718  elpreima  5722  fsn  5775  fconst2g  5822  elunirn  5858  f1ocnvfvb  5872  foeqcnvco  5882  f1eqcocnv  5883  fliftfun  5888  isose  5913  isopo  5915  isoso  5917  f1oiso2  5919  eusvobj2  5953  oprabid  5999  f1opw2  6175  op1steq  6288  rntpos  6366  frecabcl  6508  nnsucelsuc  6600  nnsucsssuc  6601  nnsseleq  6610  nnaord  6618  nnmord  6626  nnaordex  6637  nnawordex  6638  nnm00  6639  erexb  6668  swoord1  6672  swoord2  6673  iinerm  6717  fundmen  6922  mapxpen  6970  ssenen  6973  nneneq  6979  nndomo  6986  fidifsnen  6993  en1eqsnbi  7077  suplub2ti  7129  isoti  7135  ordiso2  7163  ordiso  7164  ctm  7237  ctssdc  7241  enomni  7267  enmkv  7290  enwomni  7298  pm54.43  7324  pr2ne  7326  ltexnqq  7556  genprndl  7669  genprndu  7670  nqprl  7699  nqpru  7700  1idprl  7738  1idpru  7739  ltexprlemrnd  7753  ltaprg  7767  recexprlemrnd  7777  cauappcvgprlemrnd  7798  caucvgprlemrnd  7821  caucvgprprlemrnd  7849  suplocexprlemrl  7865  suplocexprlemru  7867  map2psrprg  7953  ltxrlt  8173  lttri3  8187  addlsub  8477  addid0  8480  ltadd2  8527  eqord1  8591  reapti  8687  apreap  8695  ltmul1  8700  apreim  8711  ltleap  8740  mulap0b  8763  recapb  8779  apmul1  8896  rerecapb  8951  lt2msq  8994  nnsub  9110  zltnle  9453  zleloe  9454  zrevaddcl  9458  zltp1le  9462  zapne  9482  nn0n0n1ge2b  9487  zdiv  9496  nneo  9511  zeo2  9514  qrevaddcl  9800  npnflt  9972  nmnfgt  9975  xltneg  9993  xleadd1  10032  iccid  10082  zltaddlt1le  10164  fzn  10199  0fz1  10202  uzsplit  10249  fzm1  10257  fzrevral  10262  ssfzo12bi  10391  qltnle  10423  ioo0  10439  ioom  10440  ico0  10441  ioc0  10442  flqge  10462  modqid2  10533  modqmuladd  10548  frec2uzlt2d  10586  seqf1oglem1  10701  qsqeqor  10832  nn0ltexp2  10891  len0nnbi  11065  ccats1pfxeqbi  11233  reuccatpfxs1  11238  shftlem  11242  shftuz  11243  caucvgrelemcau  11406  sqrtsq  11470  abs00ap  11488  cau3lem  11540  maxleb  11642  rexico  11647  negfi  11654  climshft  11730  zsumdc  11810  fsum3  11813  fsum00  11888  zproddc  12005  fprodseq  12009  dvdsval2  12216  moddvds  12225  negdvdsb  12233  dvdsnegb  12234  dvdscmulr  12246  dvdsmulcr  12247  dvdssub2  12261  fzo0dvdseq  12283  ltoddhalfle  12319  dvdsgcdb  12449  gcdzeq  12458  dvdssqlem  12466  lcmeq0  12508  lcmdvdsb  12521  coprmgcdb  12525  ncoprmgcdne1b  12526  cncongr  12542  isprm2lem  12553  dvdsprime  12559  dvdsprm  12574  coprm  12581  euclemma  12583  rpexp  12590  prmdiveq  12673  hashgcdlem  12675  odzdvds  12683  pythagtrip  12721  pcdvdsb  12758  pc2dvds  12768  pcprmpw2  12771  pcprmpw  12772  enct  12919  intopsn  13314  gsumfzval  13338  isgrpid2  13487  isgrpinv  13501  f1ghm0to0  13723  ringinvnz1ne0  13926  ringinvnzdiv  13927  unitmulclb  13991  dvreq1  14019  isnzr2  14061  rrgeq0  14142  domneq0  14149  lssats2  14291  lspsneq0  14303  znunit  14536  toponcomb  14615  tgss3  14665  isopn3  14712  neiint  14732  neipsm  14741  opnneissb  14742  opnssneib  14743  tpnei  14747  opnneiid  14751  restopnb  14768  tgcn  14795  tgcnp  14796  iscnp4  14805  cnpnei  14806  cnntr  14812  lmss  14833  upxp  14859  txcn  14862  txlm  14866  hmeoopn  14898  hmeocld  14899  xblm  15004  blssexps  15016  blssex  15017  isxms2  15039  neibl  15078  metss  15081  metrest  15093  metcnp3  15098  ivthinclemlr  15224  ivthinclemur  15226  cnplimccntop  15257  eflt  15362  dvdsppwf1o  15576  lgsdir2lem4  15623  lgsne0  15630  gausslemma2dlem1a  15650  lgsquadlem1  15669  m1lgs  15677  uhgr0vb  15795  bj-charfunbi  15946  dom1o  16128  subctctexmid  16139  triap  16170  iswomni0  16192