Theorem 2thd 267

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 265	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒)))
4	1, 2, 3	sylc 65	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  2falsed  379  biort  932  vtocl2d  3557  vtocl2  3561  vtocl3  3563  rspcime  3627  sbc2or  3781  ralidm  4455  disjprgw  5061  disjprg  5062  euotd  5403  posn  5637  frsn  5639  cnvpo  6138  elabrex  7002  riota5f  7142  smoord  8002  brwdom2  9037  finacn  9476  acacni  9566  dfac13  9568  fin1a2lem10  9831  gch2  10097  gchac  10103  recmulnq  10386  nn1m1nn  11659  nn0sub  11948  xnn0n0n1ge2b  12527  qextltlem  12596  xnn0lem1lt  12638  xsubge0  12655  xlesubadd  12657  iccshftr  12873  iccshftl  12875  iccdil  12877  icccntr  12879  fzaddel  12942  elfzomelpfzo  13142  sqlecan  13572  nnesq  13589  hashdom  13741  swrdspsleq  14027  repswsymballbi  14142  m1exp1  15727  bitsmod  15785  dvdssq  15911  pcdvdsb  16205  vdwmc2  16315  acsfn  16930  subsubc  17123  funcres2b  17167  isipodrs  17771  issubg3  18297  sdrgacs  19580  opnnei  21728  lmss  21906  lmres  21908  cmpfi  22016  xkopt  22263  acufl  22525  lmhmclm  23691  equivcmet  23920  degltlem1  24666  mdegle0  24671  cxple2  25280  rlimcnp3  25545  dchrelbas3  25814  tgcolg  26340  hlbtwn  26397  eupth2lem3lem6  28012  isoun  30437  smatrcl  31061  msrrcl  32790  fz0n  32962  onint1  33797  bj-animbi  33894  bj-nfcsym  34218  matunitlindf  34905  ftc1anclem6  34987  lcvexchlem1  36185  ltrnatb  37288  cdlemg27b  37847  lmhmlvec  39168  gicabl  39719  dfacbasgrp  39728  rp-fakeimass  39898  or3or  40391  radcnvrat  40666  elabrexg  41323  eliooshift  41802  ellimcabssub0  41918