Theorem syl3an2 1168

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 1102	. . 3 ⊢ (ψ → (χ → (θ → τ)))
4	1, 3	syl5 28	. 2 ⊢ (ψ → (φ → (θ → τ)))
5	4	3imp 1097	1 ⊢ ((ψ ∧ φ ∧ θ) → τ)

Syntax hints:   → wi 4   ∧ w3a 884

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 886

This theorem is referenced by:  syl3an2b  1171  syl3an2br  1174  syl3anl2  1183  nndi  6004  nnmass  6005  prarloclemarch2  6402  1idprl  6566  1idpru  6567  recexprlem1ssl  6605  recexprlem1ssu  6606  msqge0  7400  mulge0  7403  divsubdirap  7466  divdiv32ap  7478  peano2uz  8302  fzoshftral  8864  expdivap  8959  redivap  9102  imdivap  9109