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  3748  nrmod  3839  disjprg  5099  euotd  5490  posn  5741  frsn  5743  cnvpo  6285  elabrex  7239  elabrexg  7240  riota5f  7398  smoord  8354  brwdom2  9545  finacn  10053  acacni  10143  dfac13  10145  fin1a2lem10  10411  gch2  10684  gchac  10690  recmulnq  10973  nn1m1nn  12278  nn0sub  12578  xnn0n0n1ge2b  13183  qextltlem  13254  xnn0lem1lt  13296  xsubge0  13313  xlesubadd  13315  iccshftr  13539  iccshftl  13541  iccdil  13543  icccntr  13545  fzaddel  13613  elfzomelpfzo  13828  sqlecan  14273  nnesq  14291  hashdom  14443  swrdspsleq  14735  repswsymballbi  14851  m1exp1  16466  bitsmod  16526  dvdssq  16657  pcdvdsb  16961  vdwmc2  17071  acsfn  17747  subsubc  17942  funcres2b  17986  isipodrs  18625  issubg3  19268  sdrgacs  20967  lmhmlvec  21294  matunitlindf  22903  opnnei  23345  lmss  23523  lmres  23525  cmpfi  23633  xkopt  23881  acufl  24143  lmhmclm  25315  equivcmet  25545  degltlem1  26297  mdegle0  26302  cxple2  26934  rlimcnp3  27204  dchrelbas3  27474  tgcolg  28896  hlbtwn  28956  eupth2lem3lem6  30713  ifnebib  33024  isoun  33174  subsdrg  33739  unitprodclb  33822  smatrcl  34306  msrrcl  36122  fz0n  36310  onint1  37068  bj-animbi  37259  bj-nfcsym  37642  ftc1anclem6  38447  lcvexchlem1  39907  ltrnatb  41010  cdlemg27b  41569  dvdsexpnn0  43209  fsuppind  43436  gicabl  43940  dfacbasgrp  43949  rp-fakeimass  44352  or3or  44863  radcnvrat  45138  eliooshift  46336  ellimcabssub0  46447  resccat  50000