Theorem 2thd 264

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  2falsed  376  biort  934  vtocl2d  3544  vtocl2  3551  vtocl3  3552  rspcime  3615  sbc2or  3785  ralidmOLD  4514  disjprgw  5142  disjprg  5143  euotd  5512  posn  5759  frsn  5761  cnvpo  6283  elabrex  7238  riota5f  7390  smoord  8361  brwdom2  9564  finacn  10041  acacni  10131  dfac13  10133  fin1a2lem10  10400  gch2  10666  gchac  10672  recmulnq  10955  nn1m1nn  12229  nn0sub  12518  xnn0n0n1ge2b  13107  qextltlem  13177  xnn0lem1lt  13219  xsubge0  13236  xlesubadd  13238  iccshftr  13459  iccshftl  13461  iccdil  13463  icccntr  13465  fzaddel  13531  elfzomelpfzo  13732  sqlecan  14169  nnesq  14186  hashdom  14335  swrdspsleq  14611  repswsymballbi  14726  m1exp1  16315  bitsmod  16373  dvdssq  16500  pcdvdsb  16798  vdwmc2  16908  acsfn  17599  subsubc  17799  funcres2b  17843  isipodrs  18486  issubg3  19018  sdrgacs  20409  lmhmlvec  20712  opnnei  22615  lmss  22793  lmres  22795  cmpfi  22903  xkopt  23150  acufl  23412  lmhmclm  24594  equivcmet  24825  degltlem1  25581  mdegle0  25586  cxple2  26196  rlimcnp3  26461  dchrelbas3  26730  tgcolg  27794  hlbtwn  27851  eupth2lem3lem6  29475  ifnebib  31768  isoun  31910  smatrcl  32764  msrrcl  34522  fz0n  34688  onint1  35322  bj-animbi  35423  bj-nfcsym  35767  matunitlindf  36474  ftc1anclem6  36554  lcvexchlem1  37892  ltrnatb  38996  cdlemg27b  39555  fsuppind  41159  dvdsexpnn0  41227  gicabl  41826  dfacbasgrp  41835  rp-fakeimass  42248  or3or  42759  radcnvrat  43058  elabrexg  43713  eliooshift  44205  ellimcabssub0  44319