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  3561  vtocl2  3565  vtocl3  3566  rspcime  3626  sbc2or  3799  disjprg  5143  euotd  5522  posn  5773  frsn  5775  cnvpo  6308  elabrex  7261  elabrexg  7262  riota5f  7415  smoord  8403  brwdom2  9610  finacn  10087  acacni  10178  dfac13  10180  fin1a2lem10  10446  gch2  10712  gchac  10718  recmulnq  11001  nn1m1nn  12284  nn0sub  12573  xnn0n0n1ge2b  13170  qextltlem  13240  xnn0lem1lt  13282  xsubge0  13299  xlesubadd  13301  iccshftr  13522  iccshftl  13524  iccdil  13526  icccntr  13528  fzaddel  13594  elfzomelpfzo  13806  sqlecan  14244  nnesq  14262  hashdom  14414  swrdspsleq  14699  repswsymballbi  14814  m1exp1  16409  bitsmod  16469  dvdssq  16600  pcdvdsb  16902  vdwmc2  17012  acsfn  17703  subsubc  17903  funcres2b  17947  isipodrs  18594  issubg3  19174  sdrgacs  20818  lmhmlvec  21126  opnnei  23143  lmss  23321  lmres  23323  cmpfi  23431  xkopt  23678  acufl  23940  lmhmclm  25133  equivcmet  25364  degltlem1  26125  mdegle0  26130  cxple2  26753  rlimcnp3  27024  dchrelbas3  27296  tgcolg  28576  hlbtwn  28633  eupth2lem3lem6  30261  ifnebib  32569  isoun  32716  unitprodclb  33396  smatrcl  33756  msrrcl  35527  fz0n  35710  onint1  36431  bj-animbi  36541  bj-nfcsym  36881  matunitlindf  37604  ftc1anclem6  37684  lcvexchlem1  39015  ltrnatb  40119  cdlemg27b  40678  dvdsexpnn0  42347  fsuppind  42576  gicabl  43087  dfacbasgrp  43096  rp-fakeimass  43501  or3or  44012  radcnvrat  44309  eliooshift  45458  ellimcabssub0  45572