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  3444  ralidm  4075  disjprg  4648  euotd  4975  posn  5187  frsn  5189  cnvpo  5673  elabrex  6501  riota5f  6636  smoord  7462  brwdom2  8478  finacn  8873  acacni  8962  dfac13  8964  fin1a2lem10  9231  gch2  9497  gchac  9503  recmulnq  9786  nn1m1nn  11040  nn0sub  11343  xnn0n0n1ge2b  11965  qextltlem  12033  xsubge0  12091  xlesubadd  12093  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  fzaddel  12375  elfzomelpfzo  12572  sqlecan  12971  nnesq  12988  hashdom  13168  swrdspsleq  13449  repswsymballbi  13527  znnenlem  14940  m1exp1  15093  bitsmod  15158  dvdssq  15280  pcdvdsb  15573  vdwmc2  15683  acsfn  16320  subsubc  16513  funcres2b  16557  isipodrs  17161  issubg3  17612  opnnei  20924  lmss  21102  lmres  21104  cmpfi  21211  xkopt  21458  acufl  21721  lmhmclm  22887  equivcmet  23114  degltlem1  23832  mdegle0  23837  cxple2  24443  rlimcnp3  24694  dchrelbas3  24963  tgcolg  25449  hlbtwn  25506  eupth2lem3lem6  27093  isoun  29479  smatrcl  29862  msrrcl  31440  fz0n  31616  onint1  32448  bj-nfcsym  32886  matunitlindf  33407  ftc1anclem6  33490  lcvexchlem1  34321  ltrnatb  35423  cdlemg27b  35984  gicabl  37669  dfacbasgrp  37678  sdrgacs  37771  rp-fakeimass  37857  or3or  38319  radcnvrat  38513  elabrexg  39206  eliooshift  39729  ellimcabssub0  39849