Theorem 2thd 265

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  2falsed  376  biort  935  vtocl2d  3531  vtocl2  3535  vtocl3  3536  rspcime  3596  sbc2or  3765  disjprg  5106  euotd  5476  posn  5727  frsn  5729  cnvpo  6263  elabrex  7219  elabrexg  7220  riota5f  7375  smoord  8337  brwdom2  9533  finacn  10010  acacni  10101  dfac13  10103  fin1a2lem10  10369  gch2  10635  gchac  10641  recmulnq  10924  nn1m1nn  12214  nn0sub  12499  xnn0n0n1ge2b  13099  qextltlem  13169  xnn0lem1lt  13211  xsubge0  13228  xlesubadd  13230  iccshftr  13454  iccshftl  13456  iccdil  13458  icccntr  13460  fzaddel  13526  elfzomelpfzo  13739  sqlecan  14181  nnesq  14199  hashdom  14351  swrdspsleq  14637  repswsymballbi  14752  m1exp1  16353  bitsmod  16413  dvdssq  16544  pcdvdsb  16847  vdwmc2  16957  acsfn  17627  subsubc  17822  funcres2b  17866  isipodrs  18503  issubg3  19083  sdrgacs  20717  lmhmlvec  21024  opnnei  23014  lmss  23192  lmres  23194  cmpfi  23302  xkopt  23549  acufl  23811  lmhmclm  24994  equivcmet  25224  degltlem1  25984  mdegle0  25989  cxple2  26613  rlimcnp3  26884  dchrelbas3  27156  tgcolg  28488  hlbtwn  28545  eupth2lem3lem6  30169  ifnebib  32485  isoun  32632  subsdrg  33255  unitprodclb  33367  smatrcl  33793  msrrcl  35537  fz0n  35725  onint1  36444  bj-animbi  36554  bj-nfcsym  36894  matunitlindf  37619  ftc1anclem6  37699  lcvexchlem1  39034  ltrnatb  40138  cdlemg27b  40697  dvdsexpnn0  42329  fsuppind  42585  gicabl  43095  dfacbasgrp  43104  rp-fakeimass  43508  or3or  44019  radcnvrat  44310  eliooshift  45511  ellimcabssub0  45622  resccat  49067