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  935  vtocl2d  3461  vtocl2  3465  vtocl3  3466  rspcime  3530  sbc2or  3689  ralidmOLD  4402  disjprgw  5025  disjprg  5026  euotd  5370  posn  5608  frsn  5610  cnvpo  6119  elabrex  7013  riota5f  7156  smoord  8031  brwdom2  9110  finacn  9550  acacni  9640  dfac13  9642  fin1a2lem10  9909  gch2  10175  gchac  10181  recmulnq  10464  nn1m1nn  11737  nn0sub  12026  xnn0n0n1ge2b  12609  qextltlem  12678  xnn0lem1lt  12720  xsubge0  12737  xlesubadd  12739  iccshftr  12960  iccshftl  12962  iccdil  12964  icccntr  12966  fzaddel  13032  elfzomelpfzo  13232  sqlecan  13663  nnesq  13680  hashdom  13832  swrdspsleq  14116  repswsymballbi  14231  m1exp1  15821  bitsmod  15879  dvdssq  16008  pcdvdsb  16305  vdwmc2  16415  acsfn  17033  subsubc  17228  funcres2b  17272  isipodrs  17887  issubg3  18415  sdrgacs  19699  opnnei  21871  lmss  22049  lmres  22051  cmpfi  22159  xkopt  22406  acufl  22668  lmhmclm  23839  equivcmet  24069  degltlem1  24825  mdegle0  24830  cxple2  25440  rlimcnp3  25705  dchrelbas3  25974  tgcolg  26500  hlbtwn  26557  eupth2lem3lem6  28170  isoun  30609  smatrcl  31318  msrrcl  33076  fz0n  33267  onint1  34276  bj-animbi  34377  bj-nfcsym  34716  matunitlindf  35398  ftc1anclem6  35478  lcvexchlem1  36671  ltrnatb  37774  cdlemg27b  38333  lmhmlvec  39842  fsuppind  39858  dvdsexpnn0  39918  gicabl  40496  dfacbasgrp  40505  rp-fakeimass  40673  or3or  41177  radcnvrat  41470  elabrexg  42127  eliooshift  42584  ellimcabssub0  42700