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 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  932  vtocl2d  3542  vtocl2  3547  vtocl3  3548  rspcime  3609  sbc2or  3779  ralidmOLD  4508  disjprgw  5134  disjprg  5135  euotd  5504  posn  5752  frsn  5754  cnvpo  6277  elabrex  7234  elabrexg  7235  riota5f  7387  smoord  8361  brwdom2  9565  finacn  10042  acacni  10132  dfac13  10134  fin1a2lem10  10401  gch2  10667  gchac  10673  recmulnq  10956  nn1m1nn  12231  nn0sub  12520  xnn0n0n1ge2b  13109  qextltlem  13179  xnn0lem1lt  13221  xsubge0  13238  xlesubadd  13240  iccshftr  13461  iccshftl  13463  iccdil  13465  icccntr  13467  fzaddel  13533  elfzomelpfzo  13734  sqlecan  14171  nnesq  14188  hashdom  14337  swrdspsleq  14613  repswsymballbi  14728  m1exp1  16318  bitsmod  16376  dvdssq  16503  pcdvdsb  16803  vdwmc2  16913  acsfn  17604  subsubc  17804  funcres2b  17848  isipodrs  18494  issubg3  19063  sdrgacs  20644  lmhmlvec  20950  opnnei  22948  lmss  23126  lmres  23128  cmpfi  23236  xkopt  23483  acufl  23745  lmhmclm  24938  equivcmet  25169  degltlem1  25932  mdegle0  25937  cxple2  26550  rlimcnp3  26818  dchrelbas3  27090  tgcolg  28277  hlbtwn  28334  eupth2lem3lem6  29958  ifnebib  32253  isoun  32395  smatrcl  33268  msrrcl  35025  fz0n  35197  onint1  35825  bj-animbi  35926  bj-nfcsym  36270  matunitlindf  36980  ftc1anclem6  37060  lcvexchlem1  38398  ltrnatb  39502  cdlemg27b  40061  fsuppind  41655  dvdsexpnn0  41733  gicabl  42355  dfacbasgrp  42364  rp-fakeimass  42777  or3or  43288  radcnvrat  43587  eliooshift  44729  ellimcabssub0  44843