Theorem syld3an3 1295

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  syld3an1  1296  syld3an2  1297  brelrng  4918  moriotass  5941  nnncan1  8328  lediv1  8962  modqval  10491  modqvalr  10492  modqcl  10493  flqpmodeq  10494  modq0  10496  modqge0  10499  modqlt  10500  modqdiffl  10502  modqdifz  10503  modqvalp1  10510  exp3val  10708  bcval4  10919  ccatval3  11078  ccatfv0  11082  ccatval1lsw  11083  ccatval21sw  11084  lswccatn0lsw  11090  pfxsuff1eqwrdeq  11175  dvdsmultr1  12217  dvdssub2  12221  divalglemeuneg  12309  ndvdsadd  12317  grpsubf  13486  grpinvsub  13489  grpnpcan  13499  mulginvcom  13558  mulginvinv  13559  subgsubcl  13596  qussub  13648  ghmsub  13662  dvrcl  13972  unitdvcl  13973  basgen2  14628  opnneiss  14705  cnpf2  14754  sincosq1lem  15372