Theorem syld3an3 1294

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 999	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1000	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1249	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  syld3an1  1295  syld3an2  1296  brelrng  4897  moriotass  5906  nnncan1  8262  lediv1  8896  modqval  10416  modqvalr  10417  modqcl  10418  flqpmodeq  10419  modq0  10421  modqge0  10424  modqlt  10425  modqdiffl  10427  modqdifz  10428  modqvalp1  10435  exp3val  10633  bcval4  10844  dvdsmultr1  11996  dvdssub2  12000  divalglemeuneg  12088  ndvdsadd  12096  grpsubf  13211  grpinvsub  13214  grpnpcan  13224  mulginvcom  13277  mulginvinv  13278  subgsubcl  13315  qussub  13367  ghmsub  13381  dvrcl  13691  unitdvcl  13692  basgen2  14317  opnneiss  14394  cnpf2  14443  sincosq1lem  15061