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  376  biort  934  vtocl2d  3544  vtocl2  3551  vtocl3  3552  rspcime  3616  sbc2or  3786  ralidmOLD  4515  disjprgw  5143  disjprg  5144  euotd  5513  posn  5761  frsn  5763  cnvpo  6286  elabrex  7244  riota5f  7396  smoord  8367  brwdom2  9570  finacn  10047  acacni  10137  dfac13  10139  fin1a2lem10  10406  gch2  10672  gchac  10678  recmulnq  10961  nn1m1nn  12235  nn0sub  12524  xnn0n0n1ge2b  13113  qextltlem  13183  xnn0lem1lt  13225  xsubge0  13242  xlesubadd  13244  iccshftr  13465  iccshftl  13467  iccdil  13469  icccntr  13471  fzaddel  13537  elfzomelpfzo  13738  sqlecan  14175  nnesq  14192  hashdom  14341  swrdspsleq  14617  repswsymballbi  14732  m1exp1  16321  bitsmod  16379  dvdssq  16506  pcdvdsb  16804  vdwmc2  16914  acsfn  17605  subsubc  17805  funcres2b  17849  isipodrs  18492  issubg3  19026  sdrgacs  20421  lmhmlvec  20726  opnnei  22631  lmss  22809  lmres  22811  cmpfi  22919  xkopt  23166  acufl  23428  lmhmclm  24610  equivcmet  24841  degltlem1  25597  mdegle0  25602  cxple2  26212  rlimcnp3  26479  dchrelbas3  26748  tgcolg  27843  hlbtwn  27900  eupth2lem3lem6  29524  ifnebib  31819  isoun  31961  smatrcl  32845  msrrcl  34603  fz0n  34775  onint1  35426  bj-animbi  35527  bj-nfcsym  35871  matunitlindf  36578  ftc1anclem6  36658  lcvexchlem1  37996  ltrnatb  39100  cdlemg27b  39659  fsuppind  41250  dvdsexpnn0  41320  gicabl  41929  dfacbasgrp  41938  rp-fakeimass  42351  or3or  42862  radcnvrat  43161  elabrexg  43816  eliooshift  44304  ellimcabssub0  44418