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  936  vtocl2d  3507  rspcime  3569  sbc2or  3737  disjprg  5081  euotd  5467  posn  5717  frsn  5719  cnvpo  6251  elabrex  7197  elabrexg  7198  riota5f  7352  smoord  8305  brwdom2  9488  finacn  9972  acacni  10063  dfac13  10065  fin1a2lem10  10331  gch2  10598  gchac  10604  recmulnq  10887  nn1m1nn  12195  nn0sub  12487  xnn0n0n1ge2b  13083  qextltlem  13154  xnn0lem1lt  13196  xsubge0  13213  xlesubadd  13215  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  fzaddel  13512  elfzomelpfzo  13727  sqlecan  14171  nnesq  14189  hashdom  14341  swrdspsleq  14628  repswsymballbi  14742  m1exp1  16345  bitsmod  16405  dvdssq  16536  pcdvdsb  16840  vdwmc2  16950  acsfn  17625  subsubc  17820  funcres2b  17864  isipodrs  18503  issubg3  19120  sdrgacs  20778  lmhmlvec  21105  opnnei  23085  lmss  23263  lmres  23265  cmpfi  23373  xkopt  23620  acufl  23882  lmhmclm  25054  equivcmet  25284  degltlem1  26037  mdegle0  26042  cxple2  26661  rlimcnp3  26931  dchrelbas3  27201  tgcolg  28622  hlbtwn  28679  eupth2lem3lem6  30303  ifnebib  32619  isoun  32775  subsdrg  33359  unitprodclb  33449  smatrcl  33940  msrrcl  35725  fz0n  35913  onint1  36631  bj-animbi  36823  bj-nfcsym  37206  matunitlindf  37939  ftc1anclem6  38019  lcvexchlem1  39480  ltrnatb  40583  cdlemg27b  41142  dvdsexpnn0  42766  fsuppind  43023  gicabl  43527  dfacbasgrp  43536  rp-fakeimass  43939  or3or  44450  radcnvrat  44741  eliooshift  45936  ellimcabssub0  46047  resccat  49549