Theorem 2thd 268

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 266	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒)))
4	1, 2, 3	sylc 66	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  2falsed  379  biort  948  vtocl2d  3537  rspcime  3595  sbc2or  3762  disjprg  5106  euotd  5494  posn  5745  frsn  5747  cnvpo  6285  elabrex  7238  elabrexg  7239  riota5f  7393  smoord  8348  brwdom2  9531  finacn  10030  acacni  10120  dfac13  10122  fin1a2lem10  10389  gch2  10656  gchac  10662  recmulnq  10945  nn1m1nn  12250  nn0sub  12550  xnn0n0n1ge2b  13153  qextltlem  13224  xnn0lem1lt  13266  xsubge0  13283  xlesubadd  13285  iccshftr  13509  iccshftl  13511  iccdil  13513  icccntr  13515  fzaddel  13582  elfzomelpfzo  13797  sqlecan  14241  nnesq  14259  hashdom  14411  swrdspsleq  14699  repswsymballbi  14813  m1exp1  16430  bitsmod  16490  dvdssq  16621  pcdvdsb  16925  vdwmc2  17035  acsfn  17711  subsubc  17906  funcres2b  17950  isipodrs  18589  issubg3  19207  sdrgacs  20878  lmhmlvec  21205  opnnei  23242  lmss  23420  lmres  23422  cmpfi  23530  xkopt  23777  acufl  24039  lmhmclm  25211  equivcmet  25441  degltlem1  26194  mdegle0  26199  cxple2  26824  rlimcnp3  27094  dchrelbas3  27364  tgcolg  28785  hlbtwn  28842  eupth2lem3lem6  30521  ifnebib  32832  isoun  32984  subsdrg  33558  unitprodclb  33642  smatrcl  34127  msrrcl  35930  fz0n  36118  onint1  36845  bj-animbi  37036  bj-nfcsym  37419  matunitlindf  38152  ftc1anclem6  38232  lcvexchlem1  39693  ltrnatb  40796  cdlemg27b  41355  dvdsexpnn0  42978  fsuppind  43207  gicabl  43711  dfacbasgrp  43720  rp-fakeimass  44123  or3or  44634  radcnvrat  44909  eliooshift  46107  ellimcabssub0  46218  resccat  49730