Theorem syl3an2 1308

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

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

Assertion

Ref	Expression
syl3an2	⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Proof of Theorem syl3an2

Step	Hyp	Ref	Expression
1		syl3an2.1	. . 3 ⊢ (𝜑 → 𝜒)
2		syl3an2.2	. . . 4 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
3	2	3exp 1229	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syl5 32	. 2 ⊢ (𝜓 → (𝜑 → (𝜃 → 𝜏)))
5	4	3imp 1220	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  syl3an2b  1311  syl3an2br  1314  syl3anl2  1323  nndi  6719  nnmass  6720  prarloclemarch2  7734  1idprl  7905  1idpru  7906  recexprlem1ssl  7948  recexprlem1ssu  7949  msqge0  8890  mulge0  8893  divsubdirap  8982  divdiv32ap  8994  peano2uz  9915  fzoshftral  10584  expdivap  10952  bcval5  11125  ccats1val1g  11327  redivap  11559  imdivap  11566  absdiflt  11777  absdifle  11778  retanclap  12408  tannegap  12414  lcmgcdeq  12780  isprm3  12815  prmdvdsexpb  12846  dvdsprmpweqnn  13034  mulgaddcomlem  13862  mulginvcom  13864  cnpf2  15072  blres  15299