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  3541  vtocl2  3545  vtocl3  3546  rspcime  3606  sbc2or  3774  disjprg  5115  euotd  5488  posn  5740  frsn  5742  cnvpo  6276  elabrex  7233  elabrexg  7234  riota5f  7388  smoord  8377  brwdom2  9585  finacn  10062  acacni  10153  dfac13  10155  fin1a2lem10  10421  gch2  10687  gchac  10693  recmulnq  10976  nn1m1nn  12259  nn0sub  12549  xnn0n0n1ge2b  13146  qextltlem  13216  xnn0lem1lt  13258  xsubge0  13275  xlesubadd  13277  iccshftr  13501  iccshftl  13503  iccdil  13505  icccntr  13507  fzaddel  13573  elfzomelpfzo  13785  sqlecan  14225  nnesq  14243  hashdom  14395  swrdspsleq  14681  repswsymballbi  14796  m1exp1  16393  bitsmod  16453  dvdssq  16584  pcdvdsb  16887  vdwmc2  16997  acsfn  17669  subsubc  17864  funcres2b  17908  isipodrs  18545  issubg3  19125  sdrgacs  20759  lmhmlvec  21066  opnnei  23056  lmss  23234  lmres  23236  cmpfi  23344  xkopt  23591  acufl  23853  lmhmclm  25036  equivcmet  25267  degltlem1  26027  mdegle0  26032  cxple2  26656  rlimcnp3  26927  dchrelbas3  27199  tgcolg  28479  hlbtwn  28536  eupth2lem3lem6  30160  ifnebib  32476  isoun  32625  subsdrg  33238  unitprodclb  33350  smatrcl  33773  msrrcl  35511  fz0n  35694  onint1  36413  bj-animbi  36523  bj-nfcsym  36863  matunitlindf  37588  ftc1anclem6  37668  lcvexchlem1  38998  ltrnatb  40102  cdlemg27b  40661  dvdsexpnn0  42330  fsuppind  42560  gicabl  43070  dfacbasgrp  43079  rp-fakeimass  43483  or3or  43994  radcnvrat  44286  eliooshift  45483  ellimcabssub0  45594  resccat  48989