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  667  pm5.21  696  nbn2  698  2falsed  703  pm5.21ndd  706  oibabs  715  orbi2d  791  con4biddc  858  con1bidc  875  con1bdc  879  dedlema  971  dedlemb  972  xorbin  1395  albi  1479  19.21ht  1592  exbi  1615  19.23t  1688  equequ1  1723  equequ2  1724  equsexd  1740  dral1  1741  cbv2h  1759  cbv2w  1761  sbequ12  1782  sbiedh  1798  drex1  1809  ax11b  1837  sbequ  1851  sbft  1859  sb56  1897  cbvexdh  1938  eupickb  2123  eupickbi  2124  elequ1  2168  elequ2  2169  ceqsalt  2786  ceqex  2888  mob2  2941  euxfr2dc  2946  reu6  2950  sbciegft  3017  csbiebt  3121  sseq1  3203  reupick  3444  reupick2  3446  disjeq2  4011  disjeq1  4014  exmidsssnc  4233  copsexg  4274  euotd  4284  poeq2  4332  sotritric  4356  sotritrieq  4357  seeq1  4371  seeq2  4372  alxfr  4493  ralxfrd  4494  rexxfrd  4495  ordelsuc  4538  sosng  4733  iss  4989  iotaval  5227  funeq  5275  funssres  5297  f0dom0  5448  tz6.12c  5585  fnbrfvb  5598  ssimaex  5619  fvimacnv  5674  elpreima  5678  fsn  5731  fconst2g  5774  elunirn  5810  f1ocnvfvb  5824  foeqcnvco  5834  f1eqcocnv  5835  fliftfun  5840  isose  5865  isopo  5867  isoso  5869  f1oiso2  5871  eusvobj2  5905  oprabid  5951  f1opw2  6126  op1steq  6234  rntpos  6312  frecabcl  6454  nnsucelsuc  6546  nnsucsssuc  6547  nnsseleq  6556  nnaord  6564  nnmord  6572  nnaordex  6583  nnawordex  6584  nnm00  6585  erexb  6614  swoord1  6618  swoord2  6619  iinerm  6663  fundmen  6862  mapxpen  6906  ssenen  6909  nneneq  6915  nndomo  6922  fidifsnen  6928  en1eqsnbi  7010  suplub2ti  7062  isoti  7068  ordiso2  7096  ordiso  7097  ctm  7170  ctssdc  7174  enomni  7200  enmkv  7223  enwomni  7231  pm54.43  7252  pr2ne  7254  ltexnqq  7470  genprndl  7583  genprndu  7584  nqprl  7613  nqpru  7614  1idprl  7652  1idpru  7653  ltexprlemrnd  7667  ltaprg  7681  recexprlemrnd  7691  cauappcvgprlemrnd  7712  caucvgprlemrnd  7735  caucvgprprlemrnd  7763  suplocexprlemrl  7779  suplocexprlemru  7781  map2psrprg  7867  ltxrlt  8087  lttri3  8101  addlsub  8391  addid0  8394  ltadd2  8440  eqord1  8504  reapti  8600  apreap  8608  ltmul1  8613  apreim  8624  ltleap  8653  mulap0b  8676  recapb  8692  apmul1  8809  rerecapb  8864  lt2msq  8907  nnsub  9023  zltnle  9366  zleloe  9367  zrevaddcl  9370  zltp1le  9374  zapne  9394  nn0n0n1ge2b  9399  zdiv  9408  nneo  9423  zeo2  9426  qrevaddcl  9712  npnflt  9884  nmnfgt  9887  xltneg  9905  xleadd1  9944  iccid  9994  zltaddlt1le  10076  fzn  10111  0fz1  10114  uzsplit  10161  fzm1  10169  fzrevral  10174  ssfzo12bi  10295  qltnle  10316  ioo0  10331  ioom  10332  ico0  10333  ioc0  10334  flqge  10354  modqid2  10425  modqmuladd  10440  frec2uzlt2d  10478  seqf1oglem1  10593  qsqeqor  10724  nn0ltexp2  10783  len0nnbi  10951  shftlem  10963  shftuz  10964  caucvgrelemcau  11127  sqrtsq  11191  abs00ap  11209  cau3lem  11261  maxleb  11363  rexico  11368  negfi  11374  climshft  11450  zsumdc  11530  fsum3  11533  fsum00  11608  zproddc  11725  fprodseq  11729  dvdsval2  11936  moddvds  11945  negdvdsb  11953  dvdsnegb  11954  dvdscmulr  11966  dvdsmulcr  11967  dvdssub2  11981  fzo0dvdseq  12002  ltoddhalfle  12037  dvdsgcdb  12153  gcdzeq  12162  dvdssqlem  12170  lcmeq0  12212  lcmdvdsb  12225  coprmgcdb  12229  ncoprmgcdne1b  12230  cncongr  12246  isprm2lem  12257  dvdsprime  12263  dvdsprm  12278  coprm  12285  euclemma  12287  rpexp  12294  prmdiveq  12377  hashgcdlem  12379  odzdvds  12386  pythagtrip  12424  pcdvdsb  12461  pc2dvds  12471  pcprmpw2  12474  pcprmpw  12475  enct  12593  intopsn  12953  gsumfzval  12977  isgrpid2  13115  isgrpinv  13129  f1ghm0to0  13345  ringinvnz1ne0  13548  ringinvnzdiv  13549  unitmulclb  13613  dvreq1  13641  isnzr2  13683  rrgeq0  13764  domneq0  13771  lssats2  13913  lspsneq0  13925  znunit  14158  toponcomb  14207  tgss3  14257  isopn3  14304  neiint  14324  neipsm  14333  opnneissb  14334  opnssneib  14335  tpnei  14339  opnneiid  14343  restopnb  14360  tgcn  14387  tgcnp  14388  iscnp4  14397  cnpnei  14398  cnntr  14404  lmss  14425  upxp  14451  txcn  14454  txlm  14458  hmeoopn  14490  hmeocld  14491  xblm  14596  blssexps  14608  blssex  14609  isxms2  14631  neibl  14670  metss  14673  metrest  14685  metcnp3  14690  ivthinclemlr  14816  ivthinclemur  14818  cnplimccntop  14849  eflt  14951  lgsdir2lem4  15188  lgsne0  15195  gausslemma2dlem1a  15215  lgsquadlem1  15234  m1lgs  15242  bj-charfunbi  15373  subctctexmid  15561  triap  15589  iswomni0  15611