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  666  pm5.21  695  nbn2  697  2falsed  702  pm5.21ndd  705  oibabs  714  orbi2d  790  con4biddc  857  con1bidc  874  con1bdc  878  dedlema  969  dedlemb  970  xorbin  1384  albi  1468  19.21ht  1581  exbi  1604  19.23t  1677  equequ1  1712  equequ2  1713  equsexd  1729  dral1  1730  cbv2h  1748  cbv2w  1750  sbequ12  1771  sbiedh  1787  drex1  1798  ax11b  1826  sbequ  1840  sbft  1848  sb56  1885  cbvexdh  1926  eupickb  2107  eupickbi  2108  elequ1  2152  elequ2  2153  ceqsalt  2763  ceqex  2864  mob2  2917  euxfr2dc  2922  reu6  2926  sbciegft  2993  csbiebt  3096  sseq1  3178  reupick  3419  reupick2  3421  disjeq2  3982  disjeq1  3985  exmidsssnc  4201  copsexg  4242  euotd  4252  poeq2  4298  sotritric  4322  sotritrieq  4323  seeq1  4337  seeq2  4338  alxfr  4459  ralxfrd  4460  rexxfrd  4461  ordelsuc  4502  sosng  4697  iss  4950  iotaval  5186  funeq  5233  funssres  5255  f0dom0  5406  tz6.12c  5542  fnbrfvb  5553  ssimaex  5574  fvimacnv  5628  elpreima  5632  fsn  5685  fconst2g  5728  elunirn  5762  f1ocnvfvb  5776  foeqcnvco  5786  f1eqcocnv  5787  fliftfun  5792  isose  5817  isopo  5819  isoso  5821  f1oiso2  5823  eusvobj2  5856  oprabid  5902  f1opw2  6072  op1steq  6175  rntpos  6253  frecabcl  6395  nnsucelsuc  6487  nnsucsssuc  6488  nnsseleq  6497  nnaord  6505  nnmord  6513  nnaordex  6524  nnawordex  6525  nnm00  6526  erexb  6555  swoord1  6559  swoord2  6560  iinerm  6602  fundmen  6801  mapxpen  6843  ssenen  6846  nneneq  6852  nndomo  6859  fidifsnen  6865  en1eqsnbi  6943  suplub2ti  6995  isoti  7001  ordiso2  7029  ordiso  7030  ctm  7103  ctssdc  7107  enomni  7132  enmkv  7155  enwomni  7163  pm54.43  7184  pr2ne  7186  ltexnqq  7402  genprndl  7515  genprndu  7516  nqprl  7545  nqpru  7546  1idprl  7584  1idpru  7585  ltexprlemrnd  7599  ltaprg  7613  recexprlemrnd  7623  cauappcvgprlemrnd  7644  caucvgprlemrnd  7667  caucvgprprlemrnd  7695  suplocexprlemrl  7711  suplocexprlemru  7713  map2psrprg  7799  ltxrlt  8017  lttri3  8031  addlsub  8321  addid0  8324  ltadd2  8370  eqord1  8434  reapti  8530  apreap  8538  ltmul1  8543  apreim  8554  ltleap  8583  mulap0b  8606  recapb  8622  apmul1  8739  rerecapb  8794  lt2msq  8837  nnsub  8952  zltnle  9293  zleloe  9294  zrevaddcl  9297  zltp1le  9301  zapne  9321  nn0n0n1ge2b  9326  zdiv  9335  nneo  9350  zeo2  9353  qrevaddcl  9638  npnflt  9809  nmnfgt  9812  xltneg  9830  xleadd1  9869  iccid  9919  zltaddlt1le  10001  fzn  10035  0fz1  10038  uzsplit  10085  fzm1  10093  fzrevral  10098  ssfzo12bi  10218  qltnle  10239  ioo0  10253  ioom  10254  ico0  10255  ioc0  10256  flqge  10275  modqid2  10344  modqmuladd  10359  frec2uzlt2d  10397  qsqeqor  10623  nn0ltexp2  10681  shftlem  10816  shftuz  10817  caucvgrelemcau  10980  sqrtsq  11044  abs00ap  11062  cau3lem  11114  maxleb  11216  rexico  11221  negfi  11227  climshft  11303  zsumdc  11383  fsum3  11386  fsum00  11461  zproddc  11578  fprodseq  11582  dvdsval2  11788  moddvds  11797  negdvdsb  11805  dvdsnegb  11806  dvdscmulr  11818  dvdsmulcr  11819  dvdssub2  11833  fzo0dvdseq  11853  ltoddhalfle  11888  dvdsgcdb  12004  gcdzeq  12013  dvdssqlem  12021  lcmeq0  12061  lcmdvdsb  12074  coprmgcdb  12078  ncoprmgcdne1b  12079  cncongr  12095  isprm2lem  12106  dvdsprime  12112  dvdsprm  12127  coprm  12134  euclemma  12136  rpexp  12143  prmdiveq  12226  hashgcdlem  12228  odzdvds  12235  pythagtrip  12273  pcdvdsb  12309  pc2dvds  12319  pcprmpw2  12322  pcprmpw  12323  enct  12424  intopsn  12716  isgrpid2  12841  isgrpinv  12854  ringinvnz1ne0  13126  ringinvnzdiv  13127  unitmulclb  13182  dvreq1  13210  toponcomb  13308  tgss3  13360  isopn3  13407  neiint  13427  neipsm  13436  opnneissb  13437  opnssneib  13438  tpnei  13442  opnneiid  13446  restopnb  13463  tgcn  13490  tgcnp  13491  iscnp4  13500  cnpnei  13501  cnntr  13507  lmss  13528  upxp  13554  txcn  13557  txlm  13561  hmeoopn  13593  hmeocld  13594  xblm  13699  blssexps  13711  blssex  13712  isxms2  13734  neibl  13773  metss  13776  metrest  13788  metcnp3  13793  ivthinclemlr  13897  ivthinclemur  13899  cnplimccntop  13921  eflt  13978  lgsdir2lem4  14214  lgsne0  14221  bj-charfunbi  14334  subctctexmid  14521  triap  14548  iswomni0  14570