Theorem syl6an 697

Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)

Hypotheses

Ref	Expression
syl6an.1	⊢ (𝜑 → 𝜓)
syl6an.2	⊢ (𝜑 → (𝜒 → 𝜃))
syl6an.3	⊢ ((𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl6an	⊢ (𝜑 → (𝜒 → 𝜏))

Proof of Theorem syl6an

Step	Hyp	Ref	Expression
1		syl6an.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl6an.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
3		syl6an.3	. . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
4	3	ex 418	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	1, 2, 4	sylsyld 62	1 ⊢ (𝜑 → (𝜒 → 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  dfsb2  2525  xpcan  6180  xpcan2  6181  mapxpen  9190  sucdom2  9246  inf3lem3  9658  dfac12r  10252  nnadju  10303  cfsuc  10362  fin23lem26  10430  iundom2g  10651  inar1  10887  rankcf  10889  ltsrpr  11189  supsrlem  11223  axpre-sup  11281  nominpos  12610  ublbneg  13087  qbtwnre  13356  fsequb  14145  fi1uzind  14679  brfi1indALT  14682  ccats1pfxeqrex  14892  rexanre  15543  rexuzre  15549  rexico  15550  caubnd  15555  rlim2lt  15693  rlim3  15694  lo1bddrp  15721  o1lo1  15733  climshftlem  15770  rlimcn3  15786  rlimo1  15813  lo1add  15823  lo1mul  15824  lo1le  15848  isercoll  15864  serf0  15877  cvgcmp  16012  dvds1lem  16466  dvds2lem  16467  mulmoddvds  16529  isprm5  16912  vdwlem2  17189  vdwlem10  17197  vdwlem11  17198  lsmcv  21449  lmconst  23609  ptcnplem  23970  fclscmp  24379  tsmsres  24493  addcnlem  25214  lebnumlem3  25314  xlebnum  25316  lebnumii  25317  iscmet3lem2  25643  bcthlem4  25678  cniccbdd  25812  ovoliunlem2  25854  mbfi1flimlem  26073  ply1divex  26485  aalioulem3  26691  aalioulem5  26693  aalioulem6  26694  aaliou  26695  ulmshftlem  26746  ulmbdd  26755  tanarg  26977  cxploglim  27335  ftalem2  27431  ftalem7  27436  dchrisumlem3  27848  frgrogt3nreg  31028  ubthlem3  31504  spansncol  32200  riesz1  32697  acwer1prc  35852  fineqvac  35884  j0ltaleph  36008  erdsze2lem2  36136  dfrdg4  36893  neibastop2  37327  onsuct0  37407  weiunpo  37431  bj-bary1  38425  topdifinffinlem  38462  finorwe  38497  poimirlem24  38754  incsequz  38874  caushft  38887  equivbnd  38916  cntotbnd  38922  4atexlemex4  41322  frege124d  44953  gneispace  45326  expgrowth  45511  vk15.4j  45702  sstrALT2  46008  iccpartdisj  48724  fppr2odd  49034