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  378  biort  946  vtocl2d  3527  rspcime  3585  sbc2or  3751  disjprg  5093  euotd  5479  posn  5729  frsn  5731  cnvpo  6269  elabrex  7221  elabrexg  7222  riota5f  7376  smoord  8330  brwdom2  9515  finacn  10000  acacni  10091  dfac13  10093  fin1a2lem10  10360  gch2  10627  gchac  10633  recmulnq  10916  nn1m1nn  12225  nn0sub  12525  xnn0n0n1ge2b  13128  qextltlem  13199  xnn0lem1lt  13241  xsubge0  13258  xlesubadd  13260  iccshftr  13484  iccshftl  13486  iccdil  13488  icccntr  13490  fzaddel  13557  elfzomelpfzo  13772  sqlecan  14216  nnesq  14234  hashdom  14386  swrdspsleq  14673  repswsymballbi  14787  m1exp1  16401  bitsmod  16461  dvdssq  16592  pcdvdsb  16896  vdwmc2  17006  acsfn  17682  subsubc  17877  funcres2b  17921  isipodrs  18560  issubg3  19177  sdrgacs  20838  lmhmlvec  21165  opnnei  23168  lmss  23346  lmres  23348  cmpfi  23456  xkopt  23703  acufl  23965  lmhmclm  25137  equivcmet  25367  degltlem1  26120  mdegle0  26125  cxple2  26750  rlimcnp3  27020  dchrelbas3  27290  tgcolg  28711  hlbtwn  28768  eupth2lem3lem6  30392  ifnebib  32708  isoun  32865  subsdrg  33446  unitprodclb  33536  smatrcl  34054  msrrcl  35854  fz0n  36042  onint1  36770  bj-animbi  36962  bj-nfcsym  37345  matunitlindf  38078  ftc1anclem6  38158  lcvexchlem1  39619  ltrnatb  40722  cdlemg27b  41281  dvdsexpnn0  42904  fsuppind  43133  gicabl  43637  dfacbasgrp  43646  rp-fakeimass  44049  or3or  44560  radcnvrat  44851  eliooshift  46043  ellimcabssub0  46154  resccat  49656