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  932  vtocl2d  3486  vtocl2  3490  vtocl3  3491  rspcime  3556  sbc2or  3720  ralidmOLD  4443  disjprgw  5065  disjprg  5066  euotd  5421  posn  5663  frsn  5665  cnvpo  6179  elabrex  7098  riota5f  7241  smoord  8167  brwdom2  9262  finacn  9737  acacni  9827  dfac13  9829  fin1a2lem10  10096  gch2  10362  gchac  10368  recmulnq  10651  nn1m1nn  11924  nn0sub  12213  xnn0n0n1ge2b  12796  qextltlem  12865  xnn0lem1lt  12907  xsubge0  12924  xlesubadd  12926  iccshftr  13147  iccshftl  13149  iccdil  13151  icccntr  13153  fzaddel  13219  elfzomelpfzo  13419  sqlecan  13853  nnesq  13870  hashdom  14022  swrdspsleq  14306  repswsymballbi  14421  m1exp1  16013  bitsmod  16071  dvdssq  16200  pcdvdsb  16498  vdwmc2  16608  acsfn  17285  subsubc  17484  funcres2b  17528  isipodrs  18170  issubg3  18688  sdrgacs  19984  opnnei  22179  lmss  22357  lmres  22359  cmpfi  22467  xkopt  22714  acufl  22976  lmhmclm  24156  equivcmet  24386  degltlem1  25142  mdegle0  25147  cxple2  25757  rlimcnp3  26022  dchrelbas3  26291  tgcolg  26819  hlbtwn  26876  eupth2lem3lem6  28498  isoun  30936  smatrcl  31648  msrrcl  33405  fz0n  33602  onint1  34565  bj-animbi  34666  bj-nfcsym  35011  matunitlindf  35702  ftc1anclem6  35782  lcvexchlem1  36975  ltrnatb  38078  cdlemg27b  38637  lmhmlvec  40186  fsuppind  40202  dvdsexpnn0  40262  gicabl  40840  dfacbasgrp  40849  rp-fakeimass  41017  or3or  41520  radcnvrat  41821  elabrexg  42478  eliooshift  42934  ellimcabssub0  43048