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  3523  rspcime  3581  sbc2or  3747  nrmod  3838  disjprg  5098  euotd  5485  posn  5736  frsn  5738  cnvpo  6290  elabrex  7247  elabrexg  7248  riota5f  7406  smoord  8377  brwdom2  9571  finacn  10133  acacni  10223  dfac13  10225  fin1a2lem10  10491  gch2  10764  gchac  10770  recmulnq  11053  nn1m1nn  12360  nn0sub  12660  xnn0n0n1ge2b  13265  qextltlem  13336  xnn0lem1lt  13378  xsubge0  13395  xlesubadd  13397  iccshftr  13621  iccshftl  13623  iccdil  13625  icccntr  13627  fzaddel  13696  elfzomelpfzo  13911  sqlecan  14357  nnesq  14375  hashdom  14527  swrdspsleq  14820  repswsymballbi  14936  m1exp1  16552  bitsmod  16612  dvdssq  16748  pcdvdsb  17053  vdwmc2  17163  acsfn  17839  subsubc  18034  funcres2b  18078  isipodrs  18717  issubg3  19361  sdrgacs  21064  lmhmlvec  21391  matunitlindf  23002  opnnei  23444  lmss  23622  lmres  23624  cmpfi  23732  xkopt  23980  acufl  24242  lmhmclm  25414  equivcmet  25644  degltlem1  26396  mdegle0  26401  cxple2  27031  rlimcnp3  27301  dchrelbas3  27571  tgcolg  29023  hlbtwn  29083  eupth2lem3lem6  30840  ifnebib  33193  isoun  33343  subsdrg  33907  unitprodclb  33991  smatrcl  34475  msrrcl  36395  fz0n  36589  onint1  37330  bj-animbi  37521  bj-nfcsym  37904  ftc1anclem6  38710  lcvexchlem1  40185  ltrnatb  41288  cdlemg27b  41847  dvdsexpnn0  43480  fsuppind  43712  gicabl  44195  dfacbasgrp  44204  rp-fakeimass  44607  or3or  45117  radcnvrat  45392  eliooshift  46612  ellimcabssub0  46723  resccat  50282