Theorem 2thd 268

Description: Two truths are equivalent. Deduction form. (Contributed by NM, 3-Jun-2012.)

Hypotheses

Ref	Expression
2thd.1	⊢ (𝜑 → 𝜓)
2thd.2	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
2thd	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem 2thd

Step	Hyp	Ref	Expression
1		2thd.1	. 2 ⊢ (𝜑 → 𝜓)
2		2thd.2	. 2 ⊢ (𝜑 → 𝜒)
3		pm5.1im 266	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒)))
4	1, 2, 3	sylc 65	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  2falsed  380  biort  933  vtocl2d  3505  vtocl2  3509  vtocl3  3511  rspcime  3575  sbc2or  3729  ralidm  4413  disjprgw  5025  disjprg  5026  euotd  5368  posn  5601  frsn  5603  cnvpo  6106  elabrex  6980  riota5f  7121  smoord  7985  brwdom2  9021  finacn  9461  acacni  9551  dfac13  9553  fin1a2lem10  9820  gch2  10086  gchac  10092  recmulnq  10375  nn1m1nn  11646  nn0sub  11935  xnn0n0n1ge2b  12514  qextltlem  12583  xnn0lem1lt  12625  xsubge0  12642  xlesubadd  12644  iccshftr  12864  iccshftl  12866  iccdil  12868  icccntr  12870  fzaddel  12936  elfzomelpfzo  13136  sqlecan  13567  nnesq  13584  hashdom  13736  swrdspsleq  14018  repswsymballbi  14133  m1exp1  15717  bitsmod  15775  dvdssq  15901  pcdvdsb  16195  vdwmc2  16305  acsfn  16922  subsubc  17115  funcres2b  17159  isipodrs  17763  issubg3  18289  sdrgacs  19573  opnnei  21725  lmss  21903  lmres  21905  cmpfi  22013  xkopt  22260  acufl  22522  lmhmclm  23692  equivcmet  23921  degltlem1  24673  mdegle0  24678  cxple2  25288  rlimcnp3  25553  dchrelbas3  25822  tgcolg  26348  hlbtwn  26405  eupth2lem3lem6  28018  isoun  30461  smatrcl  31149  msrrcl  32903  fz0n  33075  onint1  33910  bj-animbi  34007  bj-nfcsym  34339  matunitlindf  35055  ftc1anclem6  35135  lcvexchlem1  36330  ltrnatb  37433  cdlemg27b  37992  lmhmlvec  39452  fsuppind  39456  gicabl  40043  dfacbasgrp  40052  rp-fakeimass  40220  or3or  40724  radcnvrat  41018  elabrexg  41675  eliooshift  42143  ellimcabssub0  42259