Theorem impbid 128

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 127	. 2 ⊢ (𝜑 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm2.43i 49	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicom1  130  impbid1  141  pm5.74  178  imbi1d  230  pm5.501  243  pm5.32d  447  impbida  591  notbi  661  pm5.21  690  nbn2  692  2falsed  697  pm5.21ndd  700  oibabs  709  orbi2d  785  con4biddc  852  con1bidc  869  con1bdc  873  dedlema  964  dedlemb  965  xorbin  1379  albi  1461  19.21ht  1574  exbi  1597  19.23t  1670  equequ1  1705  equequ2  1706  equsexd  1722  dral1  1723  cbv2h  1741  cbv2w  1743  sbequ12  1764  sbiedh  1780  drex1  1791  ax11b  1819  sbequ  1833  sbft  1841  sb56  1878  cbvexdh  1919  eupickb  2100  eupickbi  2101  elequ1  2145  elequ2  2146  ceqsalt  2756  ceqex  2857  mob2  2910  euxfr2dc  2915  reu6  2919  sbciegft  2985  csbiebt  3088  sseq1  3170  reupick  3411  reupick2  3413  disjeq2  3968  disjeq1  3971  exmidsssnc  4187  copsexg  4227  euotd  4237  poeq2  4283  sotritric  4307  sotritrieq  4308  seeq1  4322  seeq2  4323  alxfr  4444  ralxfrd  4445  rexxfrd  4446  ordelsuc  4487  sosng  4682  iss  4935  iotaval  5169  funeq  5216  funssres  5238  f0dom0  5389  tz6.12c  5524  fnbrfvb  5535  ssimaex  5555  fvimacnv  5608  elpreima  5612  fsn  5665  fconst2g  5708  elunirn  5742  f1ocnvfvb  5756  foeqcnvco  5766  f1eqcocnv  5767  fliftfun  5772  isose  5797  isopo  5799  isoso  5801  f1oiso2  5803  eusvobj2  5836  oprabid  5882  f1opw2  6052  op1steq  6155  rntpos  6233  frecabcl  6375  nnsucelsuc  6467  nnsucsssuc  6468  nnsseleq  6477  nnaord  6485  nnmord  6493  nnaordex  6503  nnawordex  6504  nnm00  6505  erexb  6534  swoord1  6538  swoord2  6539  iinerm  6581  fundmen  6780  mapxpen  6822  ssenen  6825  nneneq  6831  nndomo  6838  fidifsnen  6844  en1eqsnbi  6922  suplub2ti  6974  isoti  6980  ordiso2  7008  ordiso  7009  ctm  7082  ctssdc  7086  enomni  7111  enmkv  7134  enwomni  7142  pm54.43  7154  pr2ne  7156  ltexnqq  7357  genprndl  7470  genprndu  7471  nqprl  7500  nqpru  7501  1idprl  7539  1idpru  7540  ltexprlemrnd  7554  ltaprg  7568  recexprlemrnd  7578  cauappcvgprlemrnd  7599  caucvgprlemrnd  7622  caucvgprprlemrnd  7650  suplocexprlemrl  7666  suplocexprlemru  7668  map2psrprg  7754  ltxrlt  7972  lttri3  7986  addlsub  8276  addid0  8279  ltadd2  8325  eqord1  8389  reapti  8485  apreap  8493  ltmul1  8498  apreim  8509  ltleap  8538  mulap0b  8560  apmul1  8692  lt2msq  8789  nnsub  8904  zltnle  9245  zleloe  9246  zrevaddcl  9249  zltp1le  9253  zapne  9273  nn0n0n1ge2b  9278  zdiv  9287  nneo  9302  zeo2  9305  qrevaddcl  9590  npnflt  9759  nmnfgt  9762  xltneg  9780  xleadd1  9819  iccid  9869  zltaddlt1le  9951  fzn  9985  0fz1  9988  uzsplit  10035  fzm1  10043  fzrevral  10048  ssfzo12bi  10168  qltnle  10189  ioo0  10203  ioom  10204  ico0  10205  ioc0  10206  flqge  10225  modqid2  10294  modqmuladd  10309  frec2uzlt2d  10347  qsqeqor  10573  nn0ltexp2  10631  shftlem  10767  shftuz  10768  caucvgrelemcau  10931  sqrtsq  10995  abs00ap  11013  cau3lem  11065  maxleb  11167  rexico  11172  negfi  11178  climshft  11254  zsumdc  11334  fsum3  11337  fsum00  11412  zproddc  11529  fprodseq  11533  dvdsval2  11739  moddvds  11748  negdvdsb  11756  dvdsnegb  11757  dvdscmulr  11769  dvdsmulcr  11770  dvdssub2  11784  fzo0dvdseq  11804  ltoddhalfle  11839  dvdsgcdb  11955  gcdzeq  11964  dvdssqlem  11972  lcmeq0  12012  lcmdvdsb  12025  coprmgcdb  12029  ncoprmgcdne1b  12030  cncongr  12046  isprm2lem  12057  dvdsprime  12063  dvdsprm  12078  coprm  12085  euclemma  12087  rpexp  12094  prmdiveq  12177  hashgcdlem  12179  odzdvds  12186  pythagtrip  12224  pcdvdsb  12260  pc2dvds  12270  pcprmpw2  12273  pcprmpw  12274  enct  12375  intopsn  12607  toponcomb  12741  tgss3  12793  isopn3  12840  neiint  12860  neipsm  12869  opnneissb  12870  opnssneib  12871  tpnei  12875  opnneiid  12879  restopnb  12896  tgcn  12923  tgcnp  12924  iscnp4  12933  cnpnei  12934  cnntr  12940  lmss  12961  upxp  12987  txcn  12990  txlm  12994  hmeoopn  13026  hmeocld  13027  xblm  13132  blssexps  13144  blssex  13145  isxms2  13167  neibl  13206  metss  13209  metrest  13221  metcnp3  13226  ivthinclemlr  13330  ivthinclemur  13332  cnplimccntop  13354  eflt  13411  lgsdir2lem4  13647  lgsne0  13654  bj-charfunbi  13768  subctctexmid  13956  triap  13983  iswomni0  14005