Theorem syld3an3 1283

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

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

Assertion

Ref	Expression
syld3an3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Proof of Theorem syld3an3

Step	Hyp	Ref	Expression
1		simp1 997	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 998	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1238	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  syld3an1  1284  syld3an2  1285  brelrng  4851  moriotass  5849  nnncan1  8167  lediv1  8799  modqval  10294  modqvalr  10295  modqcl  10296  flqpmodeq  10297  modq0  10299  modqge0  10302  modqlt  10303  modqdiffl  10305  modqdifz  10306  modqvalp1  10313  exp3val  10492  bcval4  10700  dvdsmultr1  11806  dvdssub2  11810  divalglemeuneg  11895  ndvdsadd  11903  grpsubf  12819  grpinvsub  12822  grpnpcan  12832  mulginvcom  12877  mulginvinv  12878  basgen2  13161  opnneiss  13238  cnpf2  13287  sincosq1lem  13826