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  935  vtocl2d  3515  vtocl2  3518  vtocl3  3519  rspcime  3577  sbc2or  3745  disjprg  5089  euotd  5456  posn  5705  frsn  5707  cnvpo  6240  elabrex  7182  elabrexg  7183  riota5f  7337  smoord  8291  brwdom2  9465  finacn  9947  acacni  10038  dfac13  10040  fin1a2lem10  10306  gch2  10572  gchac  10578  recmulnq  10861  nn1m1nn  12152  nn0sub  12437  xnn0n0n1ge2b  13037  qextltlem  13107  xnn0lem1lt  13149  xsubge0  13166  xlesubadd  13168  iccshftr  13392  iccshftl  13394  iccdil  13396  icccntr  13398  fzaddel  13464  elfzomelpfzo  13678  sqlecan  14122  nnesq  14140  hashdom  14292  swrdspsleq  14579  repswsymballbi  14693  m1exp1  16293  bitsmod  16353  dvdssq  16484  pcdvdsb  16787  vdwmc2  16897  acsfn  17571  subsubc  17766  funcres2b  17810  isipodrs  18449  issubg3  19063  sdrgacs  20722  lmhmlvec  21050  opnnei  23041  lmss  23219  lmres  23221  cmpfi  23329  xkopt  23576  acufl  23838  lmhmclm  25020  equivcmet  25250  degltlem1  26010  mdegle0  26015  cxple2  26639  rlimcnp3  26910  dchrelbas3  27182  tgcolg  28538  hlbtwn  28595  eupth2lem3lem6  30220  ifnebib  32536  isoun  32690  subsdrg  33271  unitprodclb  33361  smatrcl  33816  msrrcl  35594  fz0n  35782  onint1  36500  bj-animbi  36610  bj-nfcsym  36950  matunitlindf  37664  ftc1anclem6  37744  lcvexchlem1  39139  ltrnatb  40242  cdlemg27b  40801  dvdsexpnn0  42433  fsuppind  42689  gicabl  43197  dfacbasgrp  43206  rp-fakeimass  43610  or3or  44121  radcnvrat  44412  eliooshift  45611  ellimcabssub0  45722  resccat  49180