Theorem syl3an2 1307

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  syl3an2b  1310  syl3an2br  1313  syl3anl2  1322  nndi  6654  nnmass  6655  prarloclemarch2  7639  1idprl  7810  1idpru  7811  recexprlem1ssl  7853  recexprlem1ssu  7854  msqge0  8796  mulge0  8799  divsubdirap  8888  divdiv32ap  8900  peano2uz  9817  fzoshftral  10485  expdivap  10853  bcval5  11026  ccats1val1g  11220  redivap  11439  imdivap  11446  absdiflt  11657  absdifle  11658  retanclap  12288  tannegap  12294  lcmgcdeq  12660  isprm3  12695  prmdvdsexpb  12726  dvdsprmpweqnn  12914  mulgaddcomlem  13737  mulginvcom  13739  cnpf2  14937  blres  15164