Theorem 2thd 266

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 264	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ↔ 𝜒)))
4	1, 2, 3	sylc 65	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  2falsed  377  biort  941  vtocl2d  3507  rspcime  3565  sbc2or  3732  disjprg  5068  euotd  5454  posn  5704  frsn  5706  cnvpo  6238  elabrex  7186  elabrexg  7187  riota5f  7341  smoord  8295  brwdom2  9478  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  20773  lmhmlvec  21100  opnnei  23103  lmss  23281  lmres  23283  cmpfi  23391  xkopt  23638  acufl  23900  lmhmclm  25072  equivcmet  25302  degltlem1  26055  mdegle0  26060  cxple2  26679  rlimcnp3  26949  dchrelbas3  27219  tgcolg  28640  hlbtwn  28697  eupth2lem3lem6  30321  ifnebib  32637  isoun  32794  subsdrg  33382  unitprodclb  33472  smatrcl  33980  msrrcl  35771  fz0n  35959  onint1  36677  bj-animbi  36869  bj-nfcsym  37252  matunitlindf  37985  ftc1anclem6  38065  lcvexchlem1  39526  ltrnatb  40629  cdlemg27b  41188  dvdsexpnn0  42811  fsuppind  43040  gicabl  43544  dfacbasgrp  43553  rp-fakeimass  43956  or3or  44467  radcnvrat  44758  eliooshift  45951  ellimcabssub0  46062  resccat  49564