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  4898  moriotass  5909  nnncan1  8281  lediv1  8915  modqval  10435  modqvalr  10436  modqcl  10437  flqpmodeq  10438  modq0  10440  modqge0  10443  modqlt  10444  modqdiffl  10446  modqdifz  10447  modqvalp1  10454  exp3val  10652  bcval4  10863  dvdsmultr1  12015  dvdssub2  12019  divalglemeuneg  12107  ndvdsadd  12115  grpsubf  13283  grpinvsub  13286  grpnpcan  13296  mulginvcom  13355  mulginvinv  13356  subgsubcl  13393  qussub  13445  ghmsub  13459  dvrcl  13769  unitdvcl  13770  basgen2  14425  opnneiss  14502  cnpf2  14551  sincosq1lem  15169