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  3516  vtocl2  3519  vtocl3  3520  rspcime  3578  sbc2or  3746  disjprg  5091  euotd  5458  posn  5707  frsn  5709  cnvpo  6242  elabrex  7185  elabrexg  7186  riota5f  7340  smoord  8294  brwdom2  9470  finacn  9952  acacni  10043  dfac13  10045  fin1a2lem10  10311  gch2  10577  gchac  10583  recmulnq  10866  nn1m1nn  12157  nn0sub  12442  xnn0n0n1ge2b  13037  qextltlem  13108  xnn0lem1lt  13150  xsubge0  13167  xlesubadd  13169  iccshftr  13393  iccshftl  13395  iccdil  13397  icccntr  13399  fzaddel  13465  elfzomelpfzo  13679  sqlecan  14123  nnesq  14141  hashdom  14293  swrdspsleq  14580  repswsymballbi  14694  m1exp1  16294  bitsmod  16354  dvdssq  16485  pcdvdsb  16788  vdwmc2  16898  acsfn  17573  subsubc  17768  funcres2b  17812  isipodrs  18451  issubg3  19065  sdrgacs  20725  lmhmlvec  21053  opnnei  23055  lmss  23233  lmres  23235  cmpfi  23343  xkopt  23590  acufl  23852  lmhmclm  25034  equivcmet  25264  degltlem1  26024  mdegle0  26029  cxple2  26653  rlimcnp3  26924  dchrelbas3  27196  tgcolg  28552  hlbtwn  28609  eupth2lem3lem6  30234  ifnebib  32550  isoun  32707  subsdrg  33308  unitprodclb  33398  smatrcl  33881  msrrcl  35659  fz0n  35847  onint1  36565  bj-animbi  36675  bj-nfcsym  37016  matunitlindf  37731  ftc1anclem6  37811  lcvexchlem1  39206  ltrnatb  40309  cdlemg27b  40868  dvdsexpnn0  42504  fsuppind  42748  gicabl  43256  dfacbasgrp  43265  rp-fakeimass  43669  or3or  44180  radcnvrat  44471  eliooshift  45668  ellimcabssub0  45779  resccat  49235