Theorem 2thd 264

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 262	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒)))
4	1, 2, 3	sylc 65	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  2falsed  377  biort  933  vtocl2d  3496  vtocl2  3500  vtocl3  3501  rspcime  3564  sbc2or  3725  ralidmOLD  4446  disjprgw  5069  disjprg  5070  euotd  5427  posn  5672  frsn  5674  cnvpo  6190  elabrex  7116  riota5f  7261  smoord  8196  brwdom2  9332  finacn  9806  acacni  9896  dfac13  9898  fin1a2lem10  10165  gch2  10431  gchac  10437  recmulnq  10720  nn1m1nn  11994  nn0sub  12283  xnn0n0n1ge2b  12867  qextltlem  12936  xnn0lem1lt  12978  xsubge0  12995  xlesubadd  12997  iccshftr  13218  iccshftl  13220  iccdil  13222  icccntr  13224  fzaddel  13290  elfzomelpfzo  13491  sqlecan  13925  nnesq  13942  hashdom  14094  swrdspsleq  14378  repswsymballbi  14493  m1exp1  16085  bitsmod  16143  dvdssq  16272  pcdvdsb  16570  vdwmc2  16680  acsfn  17368  subsubc  17568  funcres2b  17612  isipodrs  18255  issubg3  18773  sdrgacs  20069  opnnei  22271  lmss  22449  lmres  22451  cmpfi  22559  xkopt  22806  acufl  23068  lmhmclm  24250  equivcmet  24481  degltlem1  25237  mdegle0  25242  cxple2  25852  rlimcnp3  26117  dchrelbas3  26386  tgcolg  26915  hlbtwn  26972  eupth2lem3lem6  28597  isoun  31034  smatrcl  31746  msrrcl  33505  fz0n  33696  onint1  34638  bj-animbi  34739  bj-nfcsym  35084  matunitlindf  35775  ftc1anclem6  35855  lcvexchlem1  37048  ltrnatb  38151  cdlemg27b  38710  lmhmlvec  40261  fsuppind  40279  dvdsexpnn0  40341  gicabl  40924  dfacbasgrp  40933  rp-fakeimass  41119  or3or  41631  radcnvrat  41932  elabrexg  42589  eliooshift  43044  ellimcabssub0  43158