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  3530  rspcime  3588  sbc2or  3755  nrmod  3846  disjprg  5107  euotd  5498  posn  5749  frsn  5751  cnvpo  6292  elabrex  7242  elabrexg  7243  riota5f  7401  smoord  8354  brwdom2  9538  finacn  10046  acacni  10136  dfac13  10138  fin1a2lem10  10404  gch2  10671  gchac  10677  recmulnq  10960  nn1m1nn  12265  nn0sub  12565  xnn0n0n1ge2b  13169  qextltlem  13240  xnn0lem1lt  13282  xsubge0  13299  xlesubadd  13301  iccshftr  13525  iccshftl  13527  iccdil  13529  icccntr  13531  fzaddel  13599  elfzomelpfzo  13814  sqlecan  14259  nnesq  14277  hashdom  14429  swrdspsleq  14721  repswsymballbi  14837  m1exp1  16452  bitsmod  16512  dvdssq  16643  pcdvdsb  16947  vdwmc2  17057  acsfn  17733  subsubc  17928  funcres2b  17972  isipodrs  18611  issubg3  19235  sdrgacs  20934  lmhmlvec  21261  opnnei  23307  lmss  23485  lmres  23487  cmpfi  23595  xkopt  23843  acufl  24105  lmhmclm  25277  equivcmet  25507  degltlem1  26260  mdegle0  26265  cxple2  26893  rlimcnp3  27163  dchrelbas3  27433  tgcolg  28854  hlbtwn  28914  eupth2lem3lem6  30631  ifnebib  32942  isoun  33094  subsdrg  33659  unitprodclb  33742  smatrcl  34226  msrrcl  36048  fz0n  36236  onint1  36993  bj-animbi  37184  bj-nfcsym  37567  matunitlindf  38302  ftc1anclem6  38382  lcvexchlem1  39841  ltrnatb  40944  cdlemg27b  41503  dvdsexpnn0  43128  fsuppind  43355  gicabl  43859  dfacbasgrp  43868  rp-fakeimass  44271  or3or  44782  radcnvrat  45057  eliooshift  46255  ellimcabssub0  46366  resccat  49885