Theorem 2thd 257

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  sbc2or  3642  ralidm  4268  disjprg  4839  euotd  5169  posn  5392  frsn  5394  cnvpo  5892  elabrex  6729  riota5f  6864  smoord  7701  brwdom2  8720  finacn  9159  acacni  9250  dfac13  9252  fin1a2lem10  9519  gch2  9785  gchac  9791  recmulnq  10074  nn1m1nn  11334  nn0sub  11632  xnn0n0n1ge2b  12212  qextltlem  12282  xsubge0  12340  xlesubadd  12342  iccshftr  12560  iccshftl  12562  iccdil  12564  icccntr  12566  fzaddel  12629  elfzomelpfzo  12827  sqlecan  13225  nnesq  13242  hashdom  13418  swrdspsleq  13703  repswsymballbi  13860  znnenlemOLD  15276  m1exp1  15429  bitsmod  15493  dvdssq  15615  pcdvdsb  15906  vdwmc2  16016  acsfn  16634  subsubc  16827  funcres2b  16871  isipodrs  17476  issubg3  17925  opnnei  21253  lmss  21431  lmres  21433  cmpfi  21540  xkopt  21787  acufl  22049  lmhmclm  23214  equivcmet  23443  degltlem1  24173  mdegle0  24178  cxple2  24784  rlimcnp3  25046  dchrelbas3  25315  tgcolg  25805  hlbtwn  25862  eupth2lem3lem6  27578  isoun  29997  smatrcl  30378  msrrcl  31957  fz0n  32130  onint1  32956  bj-nfcsym  33377  matunitlindf  33896  ftc1anclem6  33978  lcvexchlem1  35055  ltrnatb  36158  cdlemg27b  36717  gicabl  38454  dfacbasgrp  38463  sdrgacs  38556  rp-fakeimass  38641  or3or  39101  radcnvrat  39295  elabrexg  39966  eliooshift  40477  ellimcabssub0  40593