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  6515  distrnq0  6555  ltprordil  6685  1idprl  6686  1idpru  6687  ltpopr  6691  ltexprlemopu  6699  ltexprlemdisj  6702  ltexprlemfl  6705  ltexprlemfu  6707  ltexprlemru  6708  recexprlemdisj  6726  recexprlemss1l  6731  recexprlemss1u  6732  cnegexlem1  7184  msqge0  7605  mulge0  7608  divnegap  7681  divdiv32ap  7694  divneg2ap  7710  peano2uz  8524  lbzbi  8549  negqmod0  9171  expnlbnd  9371  shftfvalg  9417