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  3517  vtocl2  3521  vtocl3  3522  rspcime  3582  sbc2or  3750  disjprg  5087  euotd  5453  posn  5702  frsn  5704  cnvpo  6234  elabrex  7176  elabrexg  7177  riota5f  7331  smoord  8285  brwdom2  9459  finacn  9941  acacni  10032  dfac13  10034  fin1a2lem10  10300  gch2  10566  gchac  10572  recmulnq  10855  nn1m1nn  12146  nn0sub  12431  xnn0n0n1ge2b  13031  qextltlem  13101  xnn0lem1lt  13143  xsubge0  13160  xlesubadd  13162  iccshftr  13386  iccshftl  13388  iccdil  13390  icccntr  13392  fzaddel  13458  elfzomelpfzo  13672  sqlecan  14116  nnesq  14134  hashdom  14286  swrdspsleq  14573  repswsymballbi  14687  m1exp1  16287  bitsmod  16347  dvdssq  16478  pcdvdsb  16781  vdwmc2  16891  acsfn  17565  subsubc  17760  funcres2b  17804  isipodrs  18443  issubg3  19057  sdrgacs  20717  lmhmlvec  21045  opnnei  23036  lmss  23214  lmres  23216  cmpfi  23324  xkopt  23571  acufl  23833  lmhmclm  25015  equivcmet  25245  degltlem1  26005  mdegle0  26010  cxple2  26634  rlimcnp3  26905  dchrelbas3  27177  tgcolg  28533  hlbtwn  28590  eupth2lem3lem6  30211  ifnebib  32527  isoun  32681  subsdrg  33262  unitprodclb  33352  smatrcl  33807  msrrcl  35585  fz0n  35773  onint1  36489  bj-animbi  36599  bj-nfcsym  36939  matunitlindf  37664  ftc1anclem6  37744  lcvexchlem1  39079  ltrnatb  40182  cdlemg27b  40741  dvdsexpnn0  42373  fsuppind  42629  gicabl  43138  dfacbasgrp  43147  rp-fakeimass  43551  or3or  44062  radcnvrat  44353  eliooshift  45552  ellimcabssub0  45663  resccat  49112