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 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  2falsed  379  biort  949  vtocl2d  3527  rspcime  3585  sbc2or  3751  nrmod  3843  disjprg  5104  euotd  5493  posn  5745  frsn  5747  cnvpo  6314  elabrex  7277  elabrexg  7278  riota5f  7436  smoord  8411  brwdom2  9604  finacn  10168  acacni  10258  dfac13  10260  fin1a2lem10  10526  gch2  10799  gchac  10805  recmulnq  11088  nn1m1nn  12396  nn0sub  12696  xnn0n0n1ge2b  13301  qextltlem  13372  xnn0lem1lt  13414  xsubge0  13431  xlesubadd  13433  iccshftr  13657  iccshftl  13659  iccdil  13661  icccntr  13663  fzaddel  13732  elfzomelpfzo  13947  sqlecan  14393  nnesq  14412  hashdom  14564  swrdspsleq  14857  repswsymballbi  14973  m1exp1  16590  bitsmod  16650  dvdssq  16786  pcdvdsb  17091  vdwmc2  17201  acsfn  17883  subsubc  18078  funcres2b  18122  isipodrs  18761  issubg3  19405  sdrgacs  21109  lmhmlvec  21436  matunitlindf  23051  opnnei  23493  lmss  23671  lmres  23673  cmpfi  23781  xkopt  24029  acufl  24291  lmhmclm  25463  equivcmet  25693  degltlem1  26445  mdegle0  26450  cxple2  27082  rlimcnp3  27352  dchrelbas3  27622  tgcolg  29074  hlbtwn  29134  eupth2lem3lem6  30891  ifnebib  33243  isoun  33392  subsdrg  33964  unitprodclb  34048  smatrcl  34539  msrrcl  36516  fz0n  36711  onint1  37452  bj-animbi  37643  bj-nfcsym  38026  ftc1anclem6  38884  lcvexchlem1  40357  ltrnatb  41460  cdlemg27b  42019  dvdsexpnn0  43652  fsuppind  43884  gicabl  44367  dfacbasgrp  44375  rp-fakeimass  44774  or3or  45284  radcnvrat  45559  eliooshift  46791  ellimcabssub0  46902  resccat  50519