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  3525  vtocl2  3529  vtocl3  3530  rspcime  3590  sbc2or  3759  disjprg  5098  euotd  5468  posn  5717  frsn  5719  cnvpo  6248  elabrex  7198  elabrexg  7199  riota5f  7354  smoord  8311  brwdom2  9502  finacn  9979  acacni  10070  dfac13  10072  fin1a2lem10  10338  gch2  10604  gchac  10610  recmulnq  10893  nn1m1nn  12183  nn0sub  12468  xnn0n0n1ge2b  13068  qextltlem  13138  xnn0lem1lt  13180  xsubge0  13197  xlesubadd  13199  iccshftr  13423  iccshftl  13425  iccdil  13427  icccntr  13429  fzaddel  13495  elfzomelpfzo  13708  sqlecan  14150  nnesq  14168  hashdom  14320  swrdspsleq  14606  repswsymballbi  14721  m1exp1  16322  bitsmod  16382  dvdssq  16513  pcdvdsb  16816  vdwmc2  16926  acsfn  17596  subsubc  17791  funcres2b  17835  isipodrs  18472  issubg3  19052  sdrgacs  20686  lmhmlvec  20993  opnnei  22983  lmss  23161  lmres  23163  cmpfi  23271  xkopt  23518  acufl  23780  lmhmclm  24963  equivcmet  25193  degltlem1  25953  mdegle0  25958  cxple2  26582  rlimcnp3  26853  dchrelbas3  27125  tgcolg  28457  hlbtwn  28514  eupth2lem3lem6  30135  ifnebib  32451  isoun  32598  subsdrg  33221  unitprodclb  33333  smatrcl  33759  msrrcl  35503  fz0n  35691  onint1  36410  bj-animbi  36520  bj-nfcsym  36860  matunitlindf  37585  ftc1anclem6  37665  lcvexchlem1  39000  ltrnatb  40104  cdlemg27b  40663  dvdsexpnn0  42295  fsuppind  42551  gicabl  43061  dfacbasgrp  43070  rp-fakeimass  43474  or3or  43985  radcnvrat  44276  eliooshift  45477  ellimcabssub0  45588  resccat  49036