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 66	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  379  biort  948  vtocl2d  3529  rspcime  3587  sbc2or  3754  nrmod  3846  disjprg  5106  euotd  5498  posn  5749  frsn  5751  cnvpo  6290  elabrex  7242  elabrexg  7243  riota5f  7397  smoord  8353  brwdom2  9536  finacn  10035  acacni  10125  dfac13  10127  fin1a2lem10  10394  gch2  10661  gchac  10667  recmulnq  10950  nn1m1nn  12255  nn0sub  12555  xnn0n0n1ge2b  13158  qextltlem  13229  xnn0lem1lt  13271  xsubge0  13288  xlesubadd  13290  iccshftr  13514  iccshftl  13516  iccdil  13518  icccntr  13520  fzaddel  13588  elfzomelpfzo  13803  sqlecan  14247  nnesq  14265  hashdom  14417  swrdspsleq  14705  repswsymballbi  14819  m1exp1  16435  bitsmod  16495  dvdssq  16626  pcdvdsb  16930  vdwmc2  17040  acsfn  17716  subsubc  17911  funcres2b  17955  isipodrs  18594  issubg3  19212  sdrgacs  20885  lmhmlvec  21212  opnnei  23258  lmss  23436  lmres  23438  cmpfi  23546  xkopt  23793  acufl  24055  lmhmclm  25227  equivcmet  25457  degltlem1  26210  mdegle0  26215  cxple2  26843  rlimcnp3  27113  dchrelbas3  27383  tgcolg  28804  hlbtwn  28864  eupth2lem3lem6  30565  ifnebib  32876  isoun  33028  subsdrg  33600  unitprodclb  33683  smatrcl  34167  msrrcl  36016  fz0n  36204  onint1  36941  bj-animbi  37132  bj-nfcsym  37515  matunitlindf  38250  ftc1anclem6  38330  lcvexchlem1  39789  ltrnatb  40892  cdlemg27b  41451  dvdsexpnn0  43076  fsuppind  43305  gicabl  43809  dfacbasgrp  43818  rp-fakeimass  44221  or3or  44732  radcnvrat  45007  eliooshift  46205  ellimcabssub0  46316  resccat  49835