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  3562  vtocl2  3566  vtocl3  3567  rspcime  3627  sbc2or  3797  disjprg  5139  euotd  5518  posn  5771  frsn  5773  cnvpo  6307  elabrex  7262  elabrexg  7263  riota5f  7416  smoord  8405  brwdom2  9613  finacn  10090  acacni  10181  dfac13  10183  fin1a2lem10  10449  gch2  10715  gchac  10721  recmulnq  11004  nn1m1nn  12287  nn0sub  12576  xnn0n0n1ge2b  13174  qextltlem  13244  xnn0lem1lt  13286  xsubge0  13303  xlesubadd  13305  iccshftr  13526  iccshftl  13528  iccdil  13530  icccntr  13532  fzaddel  13598  elfzomelpfzo  13810  sqlecan  14248  nnesq  14266  hashdom  14418  swrdspsleq  14703  repswsymballbi  14818  m1exp1  16413  bitsmod  16473  dvdssq  16604  pcdvdsb  16907  vdwmc2  17017  acsfn  17702  subsubc  17898  funcres2b  17942  isipodrs  18582  issubg3  19162  sdrgacs  20802  lmhmlvec  21109  opnnei  23128  lmss  23306  lmres  23308  cmpfi  23416  xkopt  23663  acufl  23925  lmhmclm  25120  equivcmet  25351  degltlem1  26111  mdegle0  26116  cxple2  26739  rlimcnp3  27010  dchrelbas3  27282  tgcolg  28562  hlbtwn  28619  eupth2lem3lem6  30252  ifnebib  32562  isoun  32711  unitprodclb  33417  smatrcl  33795  msrrcl  35548  fz0n  35731  onint1  36450  bj-animbi  36560  bj-nfcsym  36900  matunitlindf  37625  ftc1anclem6  37705  lcvexchlem1  39035  ltrnatb  40139  cdlemg27b  40698  dvdsexpnn0  42369  fsuppind  42600  gicabl  43111  dfacbasgrp  43120  rp-fakeimass  43525  or3or  44036  radcnvrat  44333  eliooshift  45519  ellimcabssub0  45632