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  7341  isoti  7347  ordiso2  7375  ordiso  7376  ctm  7449  ctssdc  7453  enomni  7479  enmkv  7502  enwomni  7510  pm54.43  7536  pr2ne  7538  ltexnqq  7775  genprndl  7888  genprndu  7889  nqprl  7918  nqpru  7919  1idprl  7957  1idpru  7958  ltexprlemrnd  7972  ltaprg  7986  recexprlemrnd  7996  cauappcvgprlemrnd  8017  caucvgprlemrnd  8040  caucvgprprlemrnd  8068  suplocexprlemrl  8084  suplocexprlemru  8086  map2psrprg  8172  ltxrlt  8391  lttri3  8405  addlsub  8696  addid0  8699  ltadd2  8747  eqord1  8811  reapti  8907  apreap  8915  ltmul1  8920  apreim  8931  ltleap  8960  mulap0b  8983  recapb  9001  apmul1  9118  rerecapb  9173  lt2msq  9216  nnsub  9343  zltnle  9690  zleloe  9691  zrevaddcl  9695  zltp1le  9699  zapne  9719  nn0n0n1ge2b  9725  zdiv  9734  nneo  9749  zeo2  9752  qrevaddcl  10044  npnflt  10217  nmnfgt  10220  xltneg  10238  xleadd1  10277  iccid  10327  zltaddlt1le  10410  fzn  10446  0fz1  10449  uzsplit  10499  fzm1  10507  fzrevral  10512  ssfzo12bi  10643  qltnle  10678  ioo0  10694  ioom  10695  ico0  10696  ioc0  10697  flqge  10717  modqid2  10788  modqmuladd  10803  frec2uzlt2d  10841  seqf1oglem1  10956  qsqeqor  11087  nn0ltexp2  11147  hashtpg  11299  len0nnbi  11339  ccats1pfxeqbi  11514  reuccatpfxs1  11519  shftlem  11581  shftuz  11582  caucvgrelemcau  11746  sqrtsq  11810  abs00ap  11828  cau3lem  11880  maxleb  11982  rexico  11987  negfi  11994  climshft  12070  zsumdc  12151  fsum3  12154  fsum00  12229  zproddc  12346  fprodseq  12350  dvdsval2  12557  moddvds  12566  negdvdsb  12574  dvdsnegb  12575  dvdscmulr  12587  dvdsmulcr  12588  dvdssub2  12602  fzo0dvdseq  12624  ltoddhalfle  12660  dvdsgcdb  12790  gcdzeq  12799  dvdssqlem  12807  lcmeq0  12849  lcmdvdsb  12862  coprmgcdb  12866  ncoprmgcdne1b  12867  cncongr  12883  isprm2lem  12894  dvdsprime  12900  dvdsprm  12915  coprm  12922  euclemma  12924  rpexp  12931  prmdiveq  13014  hashgcdlem  13016  odzdvds  13024  pythagtrip  13062  pcdvdsb  13099  pc2dvds  13109  pcprmpw2  13112  pcprmpw  13113  enct  13324  intopsn  13687  gzsumfzval  13711  isgrpid2  13845  isgrpinv  13859  f1ghm0to0  14075  ringinvnz1ne0  14354  ringinvnzdiv  14355  unitmulclb  14421  dvreq1  14449  isnzr2  14491  rrgeq0  14573  domneq0  14581  lssats2  14751  lspsneq0  14763  znunit  14994  toponcomb  15129  tgss3  15179  isopn3  15226  neiint  15246  neipsm  15255  opnneissb  15256  opnssneib  15257  tpnei  15261  opnneiid  15265  restopnb  15282  tgcn  15309  tgcnp  15310  iscnp4  15319  cnpnei  15320  cnntr  15326  lmss  15347  upxp  15373  txcn  15376  txlm  15380  hmeoopn  15412  hmeocld  15413  xblm  15518  blssexps  15530  blssex  15531  isxms2  15553  neibl  15592  metss  15595  metrest  15607  metcnp3  15612  ivthinclemlr  15738  ivthinclemur  15740  cnplimccntop  15771  eflt  15876  dvdsppwf1o  16103  lgsdir2lem4  16150  lgsne0  16157  gausslemma2dlem1a  16177  lgsquadlem1  16196  m1lgs  16204  uhgr0vb  16325  ausgrusgrben  16409  ushgredgedg  16467  ushgredgedgloop  16469  usgr0vb  16474  loopclwwlkn1b  16660  eupth2lem3lem4fi  16714  lealltlt1  16751  lealltlt2  16752  bj-charfunbi  16837  subctctexmid  17030  stnot  17039  triap  17078  iswomni0  17101  alsralrex  17153