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  6532  frecabcl  6674  nnsucelsuc  6768  nnsucsssuc  6769  nnsseleq  6778  nnaord  6786  nnmord  6794  nnaordex  6805  nnawordex  6806  nnm00  6807  erexb  6836  swoord1  6840  swoord2  6841  iinerm  6885  mapsnd  6974  fundmen  7098  dom1o  7120  mapxpen  7152  mapunen  7155  ssenen  7156  nneneq  7162  nndomo  7169  fidifsnen  7176  en1eqsnbi  7271  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  9701  zleloe  9702  zrevaddcl  9706  zltp1le  9710  zapne  9730  nn0n0n1ge2b  9736  zdiv  9745  nneo  9760  zeo2  9763  qrevaddcl  10060  npnflt  10234  nmnfgt  10237  xltneg  10255  xleadd1  10294  iccid  10344  zltaddlt1le  10427  fzn  10463  0fz1  10466  uzsplit  10516  fzm1  10524  fzrevral  10529  ssfzo12bi  10660  qltnle  10695  ioo0  10711  ioom  10712  ico0  10713  ioc0  10714  flqge  10736  flapge  10737  modqid2  10809  modqmuladd  10824  frec2uzlt2d  10862  seqf1oglem1  10977  qsqeqor  11108  nn0ltexp2  11169  hashtpg  11321  len0nnbi  11361  ccats1pfxeqbi  11536  reuccatpfxs1  11541  shftlem  11603  shftuz  11604  caucvgrelemcau  11768  sqrtsq  11832  abs00ap  11850  cau3lem  11903  maxleb  12005  rexico  12010  negfi  12017  climshft  12095  zsumdc  12176  fsum3  12179  fsum00  12254  zproddc  12371  fprodseq  12375  dvdsval2  12582  moddvds  12591  negdvdsb  12599  dvdsnegb  12600  dvdscmulr  12612  dvdsmulcr  12613  dvdssub2  12627  fzo0dvdseq  12649  ltoddhalfle  12685  dvdsgcdb  12815  gcdzeq  12824  dvdssqlem  12832  lcmeq0  12874  lcmdvdsb  12887  coprmgcdb  12891  ncoprmgcdne1b  12892  cncongr  12908  isprm2lem  12919  dvdsprime  12925  dvdsprm  12941  coprm  12948  euclemma  12950  rpexp  12957  prmdiveq  13043  hashgcdlem  13045  odzdvds  13053  pythagtrip  13091  pcdvdsb  13128  pc2dvds  13138  pcprmpw2  13141  pcprmpw  13142  enct  13382  intopsn  13746  gzsumfzval  13770  isgrpid2  13904  isgrpinv  13918  f1ghm0to0  14134  ringinvnz1ne0  14461  ringinvnzdiv  14462  unitmulclb  14530  dvreq1  14558  isnzr2  14600  rrgeq0  14682  domneq0  14690  lssats2  14860  lspsneq0  14872  znunit  15103  toponcomb  15254  tgss3  15304  isopn3  15351  neiint  15371  neipsm  15380  opnneissb  15381  opnssneib  15382  tpnei  15386  opnneiid  15390  restopnb  15407  tgcn  15434  tgcnp  15435  iscnp4  15444  cnpnei  15445  cnntr  15451  lmss  15472  upxp  15498  txcn  15501  txlm  15505  hmeoopn  15537  hmeocld  15538  xblm  15643  blssexps  15655  blssex  15656  isxms2  15678  neibl  15717  metss  15720  metrest  15732  metcnp3  15737  ivthinclemlr  15863  ivthinclemur  15865  cnplimccntop  15896  eflt  16001  logdivlt  16124  ppiqeq0  16280  dvdsppwf1o  16283  lgsdir2lem4  16355  lgsne0  16362  gausslemma2dlem1a  16382  lgsquadlem1  16401  m1lgs  16409  uhgr0vb  16530  ausgrusgrben  16614  ushgredgedg  16672  ushgredgedgloop  16674  usgr0vb  16679  loopclwwlkn1b  16865  eupth2lem3lem4fi  16919  lealltlt1  16956  lealltlt2  16957  bj-charfunbi  17042  subctctexmid  17235  stnot  17244  triap  17284  iswomni0  17308  alsralrex  17360