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  4879  moriotass  5884  nnncan1  8228  lediv1  8861  modqval  10361  modqvalr  10362  modqcl  10363  flqpmodeq  10364  modq0  10366  modqge0  10369  modqlt  10370  modqdiffl  10372  modqdifz  10373  modqvalp1  10380  exp3val  10562  bcval4  10773  dvdsmultr1  11879  dvdssub2  11883  divalglemeuneg  11969  ndvdsadd  11977  grpsubf  13046  grpinvsub  13049  grpnpcan  13059  mulginvcom  13112  mulginvinv  13113  subgsubcl  13149  qussub  13201  ghmsub  13215  dvrcl  13510  unitdvcl  13511  basgen2  14066  opnneiss  14143  cnpf2  14192  sincosq1lem  14731