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  3519  vtocl2  3522  vtocl3  3523  rspcime  3581  sbc2or  3749  disjprg  5094  euotd  5461  posn  5710  frsn  5712  cnvpo  6245  elabrex  7188  elabrexg  7189  riota5f  7343  smoord  8297  brwdom2  9478  finacn  9960  acacni  10051  dfac13  10053  fin1a2lem10  10319  gch2  10586  gchac  10592  recmulnq  10875  nn1m1nn  12166  nn0sub  12451  xnn0n0n1ge2b  13046  qextltlem  13117  xnn0lem1lt  13159  xsubge0  13176  xlesubadd  13178  iccshftr  13402  iccshftl  13404  iccdil  13406  icccntr  13408  fzaddel  13474  elfzomelpfzo  13688  sqlecan  14132  nnesq  14150  hashdom  14302  swrdspsleq  14589  repswsymballbi  14703  m1exp1  16303  bitsmod  16363  dvdssq  16494  pcdvdsb  16797  vdwmc2  16907  acsfn  17582  subsubc  17777  funcres2b  17821  isipodrs  18460  issubg3  19074  sdrgacs  20734  lmhmlvec  21062  opnnei  23064  lmss  23242  lmres  23244  cmpfi  23352  xkopt  23599  acufl  23861  lmhmclm  25043  equivcmet  25273  degltlem1  26033  mdegle0  26038  cxple2  26662  rlimcnp3  26933  dchrelbas3  27205  tgcolg  28626  hlbtwn  28683  eupth2lem3lem6  30308  ifnebib  32624  isoun  32781  subsdrg  33380  unitprodclb  33470  smatrcl  33953  msrrcl  35737  fz0n  35925  onint1  36643  bj-animbi  36759  bj-nfcsym  37100  matunitlindf  37819  ftc1anclem6  37899  lcvexchlem1  39294  ltrnatb  40397  cdlemg27b  40956  dvdsexpnn0  42589  fsuppind  42833  gicabl  43341  dfacbasgrp  43350  rp-fakeimass  43753  or3or  44264  radcnvrat  44555  eliooshift  45752  ellimcabssub0  45863  resccat  49319