Theorem 2thd 255

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  sbc2or  3596  ralidm  4216  disjprg  4782  euotd  5106  posn  5327  frsn  5329  cnvpo  5817  elabrex  6644  riota5f  6779  smoord  7615  brwdom2  8634  finacn  9073  acacni  9164  dfac13  9166  fin1a2lem10  9433  gch2  9699  gchac  9705  recmulnq  9988  nn1m1nn  11242  nn0sub  11545  xnn0n0n1ge2b  12170  qextltlem  12238  xsubge0  12296  xlesubadd  12298  iccshftr  12513  iccshftl  12515  iccdil  12517  icccntr  12519  fzaddel  12582  elfzomelpfzo  12780  sqlecan  13178  nnesq  13195  hashdom  13370  swrdspsleq  13658  repswsymballbi  13736  znnenlem  15146  m1exp1  15301  bitsmod  15366  dvdssq  15488  pcdvdsb  15780  vdwmc2  15890  acsfn  16527  subsubc  16720  funcres2b  16764  isipodrs  17369  issubg3  17820  opnnei  21145  lmss  21323  lmres  21325  cmpfi  21432  xkopt  21679  acufl  21941  lmhmclm  23106  equivcmet  23333  degltlem1  24052  mdegle0  24057  cxple2  24664  rlimcnp3  24915  dchrelbas3  25184  tgcolg  25670  hlbtwn  25727  eupth2lem3lem6  27413  isoun  29819  smatrcl  30202  msrrcl  31778  fz0n  31954  onint1  32785  bj-nfcsym  33215  matunitlindf  33740  ftc1anclem6  33822  lcvexchlem1  34843  ltrnatb  35945  cdlemg27b  36505  gicabl  38195  dfacbasgrp  38204  sdrgacs  38297  rp-fakeimass  38383  or3or  38845  radcnvrat  39039  elabrexg  39728  eliooshift  40250  ellimcabssub0  40367