Theorem syl3an1 1168

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

Hypotheses

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

Assertion

Ref	Expression
syl3an1	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Proof of Theorem syl3an1

Step	Hyp	Ref	Expression
1		syl3an1.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	3anim1i 1090	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an1.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 14	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 885

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 887

This theorem is referenced by:  syl3an1b  1171  syl3an1br  1174  wepo  4096  f1ofveu  5500  fovrnda  5644  smoiso  5917  omv  6035  oeiv  6036  nndi  6065  nnmsucr  6067  f1oen2g  6235  f1dom2g  6236  prarloclemarch2  6517  distrnq0  6557  ltprordil  6687  1idprl  6688  1idpru  6689  ltpopr  6693  ltexprlemopu  6701  ltexprlemdisj  6704  ltexprlemfl  6707  ltexprlemfu  6709  ltexprlemru  6710  recexprlemdisj  6728  recexprlemss1l  6733  recexprlemss1u  6734  cnegexlem1  7186  msqge0  7607  mulge0  7610  divnegap  7683  divdiv32ap  7696  divneg2ap  7712  peano2uz  8526  lbzbi  8551  negqmod0  9173  expnlbnd  9373  shftfvalg  9419