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  4340  copsexg  4384  euotd  4395  poeq2  4445  sotritric  4469  sotritrieq  4470  seeq1  4484  seeq2  4485  alxfr  4607  ralxfrd  4608  rexxfrd  4609  ordelsuc  4652  sosng  4848  iss  5109  iotaval  5349  funeq  5397  funssres  5420  f0dom0  5586  tz6.12c  5725  fnbrfvb  5741  ssimaex  5764  fvimacnv  5824  elpreima  5828  fsn  5880  fconst2g  5930  fndmexb  5938  elunirn  5972  f1ocnvfvb  5986  foeqcnvco  5996  f1eqcocnv  5997  fliftfun  6002  isose  6027  isopo  6029  isoso  6031  f1oiso2  6033  eusvobj2  6071  oprabid  6117  f1opw2  6296  op1steq  6413  fvn0elsuppb  6492  rntpos  6528  frecabcl  6670  nnsucelsuc  6764  nnsucsssuc  6765  nnsseleq  6774  nnaord  6782  nnmord  6790  nnaordex  6801  nnawordex  6802  nnm00  6803  erexb  6832  swoord1  6836  swoord2  6837  iinerm  6881  mapsnd  6970  fundmen  7094  dom1o  7116  mapxpen  7148  mapunen  7151  ssenen  7152  nneneq  7158  nndomo  7165  fidifsnen  7172  en1eqsnbi  7266  suplub2ti  7342  isoti  7348  ordiso2  7376  ordiso  7377  ctm  7450  ctssdc  7454  enomni  7480  enmkv  7503  enwomni  7511  pm54.43  7537  pr2ne  7539  ltexnqq  7776  genprndl  7889  genprndu  7890  nqprl  7919  nqpru  7920  1idprl  7958  1idpru  7959  ltexprlemrnd  7973  ltaprg  7987  recexprlemrnd  7997  cauappcvgprlemrnd  8018  caucvgprlemrnd  8041  caucvgprprlemrnd  8069  suplocexprlemrl  8085  suplocexprlemru  8087  map2psrprg  8173  ltxrlt  8392  lttri3  8406  addlsub  8698  addid0  8701  ltadd2  8749  eqord1  8813  reapti  8910  apreap  8918  ltmul1  8923  apreim  8934  ltleap  8963  mulap0b  8986  recapb  9004  apmul1  9121  rerecapb  9176  lt2msq  9219  nnsub  9346  zltnle  9695  zleloe  9696  zrevaddcl  9700  zltp1le  9704  zapne  9724  nn0n0n1ge2b  9730  zdiv  9739  nneo  9754  zeo2  9757  qrevaddcl  10054  npnflt  10228  nmnfgt  10231  xltneg  10249  xleadd1  10288  iccid  10338  zltaddlt1le  10421  fzn  10457  0fz1  10460  uzsplit  10510  fzm1  10518  fzrevral  10523  ssfzo12bi  10654  qltnle  10689  ioo0  10705  ioom  10706  ico0  10707  ioc0  10708  flqge  10730  flapge  10731  modqid2  10803  modqmuladd  10818  frec2uzlt2d  10856  seqf1oglem1  10971  qsqeqor  11102  nn0ltexp2  11163  hashtpg  11315  len0nnbi  11355  ccats1pfxeqbi  11530  reuccatpfxs1  11535  shftlem  11597  shftuz  11598  caucvgrelemcau  11762  sqrtsq  11826  abs00ap  11844  cau3lem  11897  maxleb  11999  rexico  12004  negfi  12011  climshft  12089  zsumdc  12170  fsum3  12173  fsum00  12248  zproddc  12365  fprodseq  12369  dvdsval2  12576  moddvds  12585  negdvdsb  12593  dvdsnegb  12594  dvdscmulr  12606  dvdsmulcr  12607  dvdssub2  12621  fzo0dvdseq  12643  ltoddhalfle  12679  dvdsgcdb  12809  gcdzeq  12818  dvdssqlem  12826  lcmeq0  12868  lcmdvdsb  12881  coprmgcdb  12885  ncoprmgcdne1b  12886  cncongr  12902  isprm2lem  12913  dvdsprime  12919  dvdsprm  12935  coprm  12942  euclemma  12944  rpexp  12951  prmdiveq  13037  hashgcdlem  13039  odzdvds  13047  pythagtrip  13085  pcdvdsb  13122  pc2dvds  13132  pcprmpw2  13135  pcprmpw  13136  enct  13376  intopsn  13740  gzsumfzval  13764  isgrpid2  13898  isgrpinv  13912  f1ghm0to0  14128  ringinvnz1ne0  14438  ringinvnzdiv  14439  unitmulclb  14505  dvreq1  14533  isnzr2  14575  rrgeq0  14657  domneq0  14665  lssats2  14835  lspsneq0  14847  znunit  15078  toponcomb  15220  tgss3  15270  isopn3  15317  neiint  15337  neipsm  15346  opnneissb  15347  opnssneib  15348  tpnei  15352  opnneiid  15356  restopnb  15373  tgcn  15400  tgcnp  15401  iscnp4  15410  cnpnei  15411  cnntr  15417  lmss  15438  upxp  15464  txcn  15467  txlm  15471  hmeoopn  15503  hmeocld  15504  xblm  15609  blssexps  15621  blssex  15622  isxms2  15644  neibl  15683  metss  15686  metrest  15698  metcnp3  15703  ivthinclemlr  15829  ivthinclemur  15831  cnplimccntop  15862  eflt  15967  logdivlt  16088  ppiqeq0  16241  dvdsppwf1o  16244  lgsdir2lem4  16316  lgsne0  16323  gausslemma2dlem1a  16343  lgsquadlem1  16362  m1lgs  16370  uhgr0vb  16491  ausgrusgrben  16575  ushgredgedg  16633  ushgredgedgloop  16635  usgr0vb  16640  loopclwwlkn1b  16826  eupth2lem3lem4fi  16880  lealltlt1  16917  lealltlt2  16918  bj-charfunbi  17003  subctctexmid  17196  stnot  17205  triap  17244  iswomni0  17268  alsralrex  17320