Theorem 2thd 254

Description: Two truths are equivalent (deduction rule). (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 252	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒)))
4	1, 2, 3	sylc 63	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  sbc2or  3411  ralidm  4027  disjprg  4578  euotd  4900  posn  5110  frsn  5112  cnvpo  5590  elabrex  6405  riota5f  6535  smoord  7349  brwdom2  8361  finacn  8756  acacni  8845  dfac13  8847  fin1a2lem10  9114  gch2  9376  gchac  9382  recmulnq  9665  nn1m1nn  10917  nn0sub  11220  xnn0n0n1ge2b  11841  qextltlem  11907  xsubge0  11963  xlesubadd  11965  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  fzaddel  12246  elfzomelpfzo  12438  sqlecan  12833  nnesq  12850  hashdom  13029  swrdspsleq  13301  repswsymballbi  13378  znnenlem  14779  m1exp1  14931  bitsmod  14996  dvdssq  15118  pcdvdsb  15411  vdwmc2  15521  acsfn  16143  subsubc  16336  funcres2b  16380  isipodrs  16984  issubg3  17435  opnnei  20734  lmss  20912  lmres  20914  cmpfi  21021  xkopt  21268  acufl  21531  lmhmclm  22695  equivcmet  22922  degltlem1  23636  mdegle0  23641  cxple2  24243  rlimcnp3  24494  dchrelbas3  24763  tgcolg  25249  hlbtwn  25306  eupath2lem3  26506  isoun  28862  smatrcl  29190  msrrcl  30694  fz0n  30869  onint1  31618  bj-nfcsym  32079  matunitlindf  32577  ftc1anclem6  32660  lcvexchlem1  33339  ltrnatb  34441  cdlemg27b  35002  gicabl  36687  dfacbasgrp  36697  sdrgacs  36790  rp-fakeimass  36876  or3or  37339  radcnvrat  37535  elabrexg  38229  eliooshift  38576  ellimcabssub0  38684  eupth2lem3lem6  41401