Theorem 2thd 265

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  2falsed  376  biort  936  vtocl2d  3521  vtocl2  3524  vtocl3  3525  rspcime  3583  sbc2or  3751  disjprg  5096  euotd  5469  posn  5718  frsn  5720  cnvpo  6253  elabrex  7198  elabrexg  7199  riota5f  7353  smoord  8307  brwdom2  9490  finacn  9972  acacni  10063  dfac13  10065  fin1a2lem10  10331  gch2  10598  gchac  10604  recmulnq  10887  nn1m1nn  12178  nn0sub  12463  xnn0n0n1ge2b  13058  qextltlem  13129  xnn0lem1lt  13171  xsubge0  13188  xlesubadd  13190  iccshftr  13414  iccshftl  13416  iccdil  13418  icccntr  13420  fzaddel  13486  elfzomelpfzo  13700  sqlecan  14144  nnesq  14162  hashdom  14314  swrdspsleq  14601  repswsymballbi  14715  m1exp1  16315  bitsmod  16375  dvdssq  16506  pcdvdsb  16809  vdwmc2  16919  acsfn  17594  subsubc  17789  funcres2b  17833  isipodrs  18472  issubg3  19086  sdrgacs  20746  lmhmlvec  21074  opnnei  23076  lmss  23254  lmres  23256  cmpfi  23364  xkopt  23611  acufl  23873  lmhmclm  25055  equivcmet  25285  degltlem1  26045  mdegle0  26050  cxple2  26674  rlimcnp3  26945  dchrelbas3  27217  tgcolg  28638  hlbtwn  28695  eupth2lem3lem6  30320  ifnebib  32635  isoun  32791  subsdrg  33391  unitprodclb  33481  smatrcl  33973  msrrcl  35756  fz0n  35944  onint1  36662  bj-animbi  36780  bj-nfcsym  37144  matunitlindf  37866  ftc1anclem6  37946  lcvexchlem1  39407  ltrnatb  40510  cdlemg27b  41069  dvdsexpnn0  42701  fsuppind  42945  gicabl  43453  dfacbasgrp  43462  rp-fakeimass  43865  or3or  44376  radcnvrat  44667  eliooshift  45863  ellimcabssub0  45974  resccat  49430