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  4342  copsexg  4386  euotd  4397  poeq2  4447  sotritric  4471  sotritrieq  4472  seeq1  4486  seeq2  4487  alxfr  4609  ralxfrd  4610  rexxfrd  4611  ordelsuc  4654  sosng  4850  iss  5112  iotaval  5352  funeq  5400  funssres  5423  f0dom0  5589  tz6.12c  5728  fnbrfvb  5744  ssimaex  5767  fvimacnv  5827  elpreima  5831  fsn  5883  fconst2g  5933  fndmexb  5941  elunirn  5975  f1ocnvfvb  5989  foeqcnvco  5999  f1eqcocnv  6000  fliftfun  6005  isose  6030  isopo  6032  isoso  6034  f1oiso2  6036  eusvobj2  6074  oprabid  6120  f1opw2  6299  op1steq  6417  fvn0elsuppb  6496  rntpos  6533  frecabcl  6675  nnsucelsuc  6769  nnsucsssuc  6770  nnsseleq  6779  nnaord  6787  nnmord  6795  nnaordex  6806  nnawordex  6807  nnm00  6808  erexb  6837  swoord1  6841  swoord2  6842  iinerm  6886  mapsnd  6976  fundmen  7100  dom1o  7122  mapxpen  7154  mapunen  7157  ssenen  7158  nneneq  7164  nndomo  7171  fidifsnen  7178  en1eqsnbi  7273  suplub2ti  7347  isoti  7353  ordiso2  7381  ordiso  7382  ctm  7455  ctssdc  7459  enomni  7485  enmkv  7508  enwomni  7516  pm54.43  7542  pr2ne  7544  ltexnqq  7781  genprndl  7894  genprndu  7895  nqprl  7924  nqpru  7925  1idprl  7963  1idpru  7964  ltexprlemrnd  7978  ltaprg  7992  recexprlemrnd  8002  cauappcvgprlemrnd  8023  caucvgprlemrnd  8046  caucvgprprlemrnd  8074  suplocexprlemrl  8090  suplocexprlemru  8092  map2psrprg  8178  ltxrlt  8397  lttri3  8411  addlsub  8703  addid0  8706  ltadd2  8754  eqord1  8818  reapti  8915  apreap  8923  ltmul1  8928  apreim  8939  ltleap  8968  mulap0b  8991  recapb  9009  apmul1  9126  rerecapb  9181  lt2msq  9224  nnsub  9352  zltnle  9699  zleloe  9700  zrevaddcl  9704  zltp1le  9708  zapne  9728  nn0n0n1ge2b  9734  zdiv  9744  nneo  9759  zeo2  9762  qrevaddcl  10059  npnflt  10233  nmnfgt  10236  xltneg  10254  xleadd1  10293  iccid  10343  zltaddlt1le  10426  fzn  10462  0fz1  10465  uzsplit  10515  fzm1  10523  fzrevral  10528  ssfzo12bi  10659  qltnle  10694  ioo0  10710  ioom  10711  ico0  10712  ioc0  10713  flqge  10735  flapge  10736  modqid2  10808  modqmuladd  10823  frec2uzlt2d  10861  seqf1oglem1  10976  qsqeqor  11107  nn0ltexp2  11168  hashtpg  11320  len0nnbi  11360  ccats1pfxeqbi  11535  reuccatpfxs1  11540  shftlem  11602  shftuz  11603  caucvgrelemcau  11767  sqrtsq  11831  abs00ap  11849  cau3lem  11902  maxleb  12004  rexico  12009  negfi  12016  climshft  12094  zsumdc  12175  fsum3  12178  fsum00  12253  zproddc  12370  fprodseq  12374  dvdsval2  12581  moddvds  12590  negdvdsb  12598  dvdsnegb  12599  dvdscmulr  12611  dvdsmulcr  12612  dvdssub2  12626  fzo0dvdseq  12648  ltoddhalfle  12684  dvdsgcdb  12814  gcdzeq  12823  dvdssqlem  12831  lcmeq0  12873  lcmdvdsb  12886  coprmgcdb  12890  ncoprmgcdne1b  12891  cncongr  12907  isprm2lem  12918  dvdsprime  12924  dvdsprm  12940  coprm  12947  euclemma  12949  rpexp  12956  prmdiveq  13042  hashgcdlem  13044  odzdvds  13052  pythagtrip  13090  pcdvdsb  13127  pc2dvds  13137  pcprmpw2  13140  pcprmpw  13141  enct  13381  intopsn  13745  gzsumfzval  13769  isgrpid2  13903  isgrpinv  13917  f1ghm0to0  14133  ringinvnz1ne0  14460  ringinvnzdiv  14461  unitmulclb  14529  dvreq1  14557  isnzr2  14599  rrgeq0  14681  domneq0  14689  lssats2  14859  lspsneq0  14871  znunit  15102  toponcomb  15271  tgss3  15321  isopn3  15368  neiint  15388  neipsm  15397  opnneissb  15398  opnssneib  15399  tpnei  15403  opnneiid  15407  restopnb  15424  tgcn  15451  tgcnp  15452  iscnp4  15461  cnpnei  15462  cnntr  15468  lmss  15489  upxp  15515  txcn  15518  txlm  15522  hmeoopn  15554  hmeocld  15555  xblm  15660  blssexps  15672  blssex  15673  isxms2  15695  neibl  15734  metss  15737  metrest  15749  metcnp3  15754  ivthinclemlr  15880  ivthinclemur  15882  cnplimccntop  15913  eflt  16018  logdivlt  16141  ppiqeq0  16297  dvdsppwf1o  16300  lgsdir2lem4  16372  lgsne0  16379  gausslemma2dlem1a  16399  lgsquadlem1  16418  m1lgs  16426  uhgr0vb  16547  ausgrusgrben  16631  ushgredgedg  16689  ushgredgedgloop  16691  usgr0vb  16696  loopclwwlkn1b  16882  eupth2lem3lem4fi  16936  lealltlt1  16973  lealltlt2  16974  bj-charfunbi  17059  subctctexmid  17252  stnot  17261  triap  17301  iswomni0  17325  alsralrex  17377