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  668  pm5.21  697  nbn2  699  2falsed  704  pm5.21ndd  707  oibabs  716  orbi2d  792  con4biddc  859  con1bidc  876  con1bdc  880  dedlema  972  dedlemb  973  xorbin  1404  albi  1491  19.21ht  1604  exbi  1627  19.23t  1700  equequ1  1735  equequ2  1736  equsexd  1752  dral1  1753  cbv2h  1771  cbv2w  1773  sbequ12  1794  sbiedh  1810  drex1  1821  ax11b  1849  sbequ  1863  sbft  1871  sb56  1909  cbvexdh  1950  eupickb  2135  eupickbi  2136  elequ1  2180  elequ2  2181  ceqsalt  2798  ceqex  2900  mob2  2953  euxfr2dc  2958  reu6  2962  sbciegft  3029  csbiebt  3133  sseq1  3216  reupick  3457  reupick2  3459  disjeq2  4025  disjeq1  4028  exmidsssnc  4247  copsexg  4288  euotd  4299  poeq2  4347  sotritric  4371  sotritrieq  4372  seeq1  4386  seeq2  4387  alxfr  4508  ralxfrd  4509  rexxfrd  4510  ordelsuc  4553  sosng  4748  iss  5005  iotaval  5243  funeq  5291  funssres  5313  f0dom0  5469  tz6.12c  5606  fnbrfvb  5619  ssimaex  5640  fvimacnv  5695  elpreima  5699  fsn  5752  fconst2g  5799  elunirn  5835  f1ocnvfvb  5849  foeqcnvco  5859  f1eqcocnv  5860  fliftfun  5865  isose  5890  isopo  5892  isoso  5894  f1oiso2  5896  eusvobj2  5930  oprabid  5976  f1opw2  6152  op1steq  6265  rntpos  6343  frecabcl  6485  nnsucelsuc  6577  nnsucsssuc  6578  nnsseleq  6587  nnaord  6595  nnmord  6603  nnaordex  6614  nnawordex  6615  nnm00  6616  erexb  6645  swoord1  6649  swoord2  6650  iinerm  6694  fundmen  6898  mapxpen  6945  ssenen  6948  nneneq  6954  nndomo  6961  fidifsnen  6967  en1eqsnbi  7051  suplub2ti  7103  isoti  7109  ordiso2  7137  ordiso  7138  ctm  7211  ctssdc  7215  enomni  7241  enmkv  7264  enwomni  7272  pm54.43  7298  pr2ne  7300  ltexnqq  7521  genprndl  7634  genprndu  7635  nqprl  7664  nqpru  7665  1idprl  7703  1idpru  7704  ltexprlemrnd  7718  ltaprg  7732  recexprlemrnd  7742  cauappcvgprlemrnd  7763  caucvgprlemrnd  7786  caucvgprprlemrnd  7814  suplocexprlemrl  7830  suplocexprlemru  7832  map2psrprg  7918  ltxrlt  8138  lttri3  8152  addlsub  8442  addid0  8445  ltadd2  8492  eqord1  8556  reapti  8652  apreap  8660  ltmul1  8665  apreim  8676  ltleap  8705  mulap0b  8728  recapb  8744  apmul1  8861  rerecapb  8916  lt2msq  8959  nnsub  9075  zltnle  9418  zleloe  9419  zrevaddcl  9423  zltp1le  9427  zapne  9447  nn0n0n1ge2b  9452  zdiv  9461  nneo  9476  zeo2  9479  qrevaddcl  9765  npnflt  9937  nmnfgt  9940  xltneg  9958  xleadd1  9997  iccid  10047  zltaddlt1le  10129  fzn  10164  0fz1  10167  uzsplit  10214  fzm1  10222  fzrevral  10227  ssfzo12bi  10354  qltnle  10386  ioo0  10402  ioom  10403  ico0  10404  ioc0  10405  flqge  10425  modqid2  10496  modqmuladd  10511  frec2uzlt2d  10549  seqf1oglem1  10664  qsqeqor  10795  nn0ltexp2  10854  len0nnbi  11028  shftlem  11127  shftuz  11128  caucvgrelemcau  11291  sqrtsq  11355  abs00ap  11373  cau3lem  11425  maxleb  11527  rexico  11532  negfi  11539  climshft  11615  zsumdc  11695  fsum3  11698  fsum00  11773  zproddc  11890  fprodseq  11894  dvdsval2  12101  moddvds  12110  negdvdsb  12118  dvdsnegb  12119  dvdscmulr  12131  dvdsmulcr  12132  dvdssub2  12146  fzo0dvdseq  12168  ltoddhalfle  12204  dvdsgcdb  12334  gcdzeq  12343  dvdssqlem  12351  lcmeq0  12393  lcmdvdsb  12406  coprmgcdb  12410  ncoprmgcdne1b  12411  cncongr  12427  isprm2lem  12438  dvdsprime  12444  dvdsprm  12459  coprm  12466  euclemma  12468  rpexp  12475  prmdiveq  12558  hashgcdlem  12560  odzdvds  12568  pythagtrip  12606  pcdvdsb  12643  pc2dvds  12653  pcprmpw2  12656  pcprmpw  12657  enct  12804  intopsn  13199  gsumfzval  13223  isgrpid2  13372  isgrpinv  13386  f1ghm0to0  13608  ringinvnz1ne0  13811  ringinvnzdiv  13812  unitmulclb  13876  dvreq1  13904  isnzr2  13946  rrgeq0  14027  domneq0  14034  lssats2  14176  lspsneq0  14188  znunit  14421  toponcomb  14500  tgss3  14550  isopn3  14597  neiint  14617  neipsm  14626  opnneissb  14627  opnssneib  14628  tpnei  14632  opnneiid  14636  restopnb  14653  tgcn  14680  tgcnp  14681  iscnp4  14690  cnpnei  14691  cnntr  14697  lmss  14718  upxp  14744  txcn  14747  txlm  14751  hmeoopn  14783  hmeocld  14784  xblm  14889  blssexps  14901  blssex  14902  isxms2  14924  neibl  14963  metss  14966  metrest  14978  metcnp3  14983  ivthinclemlr  15109  ivthinclemur  15111  cnplimccntop  15142  eflt  15247  dvdsppwf1o  15461  lgsdir2lem4  15508  lgsne0  15515  gausslemma2dlem1a  15535  lgsquadlem1  15554  m1lgs  15562  bj-charfunbi  15751  subctctexmid  15941  triap  15972  iswomni0  15994