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  934  vtocl2d  3574  vtocl2  3578  vtocl3  3579  rspcime  3640  sbc2or  3813  disjprg  5162  euotd  5532  posn  5785  frsn  5787  cnvpo  6318  elabrex  7279  elabrexg  7280  riota5f  7433  smoord  8421  brwdom2  9642  finacn  10119  acacni  10210  dfac13  10212  fin1a2lem10  10478  gch2  10744  gchac  10750  recmulnq  11033  nn1m1nn  12314  nn0sub  12603  xnn0n0n1ge2b  13194  qextltlem  13264  xnn0lem1lt  13306  xsubge0  13323  xlesubadd  13325  iccshftr  13546  iccshftl  13548  iccdil  13550  icccntr  13552  fzaddel  13618  elfzomelpfzo  13821  sqlecan  14258  nnesq  14276  hashdom  14428  swrdspsleq  14713  repswsymballbi  14828  m1exp1  16424  bitsmod  16482  dvdssq  16614  pcdvdsb  16916  vdwmc2  17026  acsfn  17717  subsubc  17917  funcres2b  17961  isipodrs  18607  issubg3  19184  sdrgacs  20824  lmhmlvec  21132  opnnei  23149  lmss  23327  lmres  23329  cmpfi  23437  xkopt  23684  acufl  23946  lmhmclm  25139  equivcmet  25370  degltlem1  26131  mdegle0  26136  cxple2  26757  rlimcnp3  27028  dchrelbas3  27300  tgcolg  28580  hlbtwn  28637  eupth2lem3lem6  30265  ifnebib  32572  isoun  32713  unitprodclb  33382  smatrcl  33742  msrrcl  35511  fz0n  35693  onint1  36415  bj-animbi  36525  bj-nfcsym  36865  matunitlindf  37578  ftc1anclem6  37658  lcvexchlem1  38990  ltrnatb  40094  cdlemg27b  40653  dvdsexpnn0  42321  fsuppind  42545  gicabl  43056  dfacbasgrp  43065  rp-fakeimass  43474  or3or  43985  radcnvrat  44283  eliooshift  45424  ellimcabssub0  45538