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  935  vtocl2d  3528  vtocl2  3532  vtocl3  3533  rspcime  3593  sbc2or  3762  disjprg  5103  euotd  5473  posn  5724  frsn  5726  cnvpo  6260  elabrex  7216  elabrexg  7217  riota5f  7372  smoord  8334  brwdom2  9526  finacn  10003  acacni  10094  dfac13  10096  fin1a2lem10  10362  gch2  10628  gchac  10634  recmulnq  10917  nn1m1nn  12207  nn0sub  12492  xnn0n0n1ge2b  13092  qextltlem  13162  xnn0lem1lt  13204  xsubge0  13221  xlesubadd  13223  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  fzaddel  13519  elfzomelpfzo  13732  sqlecan  14174  nnesq  14192  hashdom  14344  swrdspsleq  14630  repswsymballbi  14745  m1exp1  16346  bitsmod  16406  dvdssq  16537  pcdvdsb  16840  vdwmc2  16950  acsfn  17620  subsubc  17815  funcres2b  17859  isipodrs  18496  issubg3  19076  sdrgacs  20710  lmhmlvec  21017  opnnei  23007  lmss  23185  lmres  23187  cmpfi  23295  xkopt  23542  acufl  23804  lmhmclm  24987  equivcmet  25217  degltlem1  25977  mdegle0  25982  cxple2  26606  rlimcnp3  26877  dchrelbas3  27149  tgcolg  28481  hlbtwn  28538  eupth2lem3lem6  30162  ifnebib  32478  isoun  32625  subsdrg  33248  unitprodclb  33360  smatrcl  33786  msrrcl  35530  fz0n  35718  onint1  36437  bj-animbi  36547  bj-nfcsym  36887  matunitlindf  37612  ftc1anclem6  37692  lcvexchlem1  39027  ltrnatb  40131  cdlemg27b  40690  dvdsexpnn0  42322  fsuppind  42578  gicabl  43088  dfacbasgrp  43097  rp-fakeimass  43501  or3or  44012  radcnvrat  44303  eliooshift  45504  ellimcabssub0  45615  resccat  49063