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  3508  rspcime  3570  sbc2or  3738  disjprg  5082  euotd  5461  posn  5710  frsn  5712  cnvpo  6245  elabrex  7190  elabrexg  7191  riota5f  7345  smoord  8298  brwdom2  9481  finacn  9963  acacni  10054  dfac13  10056  fin1a2lem10  10322  gch2  10589  gchac  10595  recmulnq  10878  nn1m1nn  12186  nn0sub  12478  xnn0n0n1ge2b  13074  qextltlem  13145  xnn0lem1lt  13187  xsubge0  13204  xlesubadd  13206  iccshftr  13430  iccshftl  13432  iccdil  13434  icccntr  13436  fzaddel  13503  elfzomelpfzo  13718  sqlecan  14162  nnesq  14180  hashdom  14332  swrdspsleq  14619  repswsymballbi  14733  m1exp1  16336  bitsmod  16396  dvdssq  16527  pcdvdsb  16831  vdwmc2  16941  acsfn  17616  subsubc  17811  funcres2b  17855  isipodrs  18494  issubg3  19111  sdrgacs  20769  lmhmlvec  21097  opnnei  23095  lmss  23273  lmres  23275  cmpfi  23383  xkopt  23630  acufl  23892  lmhmclm  25064  equivcmet  25294  degltlem1  26047  mdegle0  26052  cxple2  26674  rlimcnp3  26944  dchrelbas3  27215  tgcolg  28636  hlbtwn  28693  eupth2lem3lem6  30318  ifnebib  32634  isoun  32790  subsdrg  33374  unitprodclb  33464  smatrcl  33956  msrrcl  35741  fz0n  35929  onint1  36647  bj-animbi  36839  bj-nfcsym  37222  matunitlindf  37953  ftc1anclem6  38033  lcvexchlem1  39494  ltrnatb  40597  cdlemg27b  41156  dvdsexpnn0  42780  fsuppind  43037  gicabl  43545  dfacbasgrp  43554  rp-fakeimass  43957  or3or  44468  radcnvrat  44759  eliooshift  45954  ellimcabssub0  46065  resccat  49561