Theorem syl3an2 1305

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 1226	. . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syl5 32	. 2 ⊢ (𝜓 → (𝜑 → (𝜃 → 𝜏)))
5	4	3imp 1217	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  syl3an2b  1308  syl3an2br  1311  syl3anl2  1320  nndi  6649  nnmass  6650  prarloclemarch2  7629  1idprl  7800  1idpru  7801  recexprlem1ssl  7843  recexprlem1ssu  7844  msqge0  8786  mulge0  8789  divsubdirap  8878  divdiv32ap  8890  peano2uz  9807  fzoshftral  10474  expdivap  10842  bcval5  11015  ccats1val1g  11206  redivap  11425  imdivap  11432  absdiflt  11643  absdifle  11644  retanclap  12273  tannegap  12279  lcmgcdeq  12645  isprm3  12680  prmdvdsexpb  12711  dvdsprmpweqnn  12899  mulgaddcomlem  13722  mulginvcom  13724  cnpf2  14921  blres  15148