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  5907  nnncan1  8264  lediv1  8898  modqval  10418  modqvalr  10419  modqcl  10420  flqpmodeq  10421  modq0  10423  modqge0  10426  modqlt  10427  modqdiffl  10429  modqdifz  10430  modqvalp1  10437  exp3val  10635  bcval4  10846  dvdsmultr1  11998  dvdssub2  12002  divalglemeuneg  12090  ndvdsadd  12098  grpsubf  13221  grpinvsub  13224  grpnpcan  13234  mulginvcom  13287  mulginvinv  13288  subgsubcl  13325  qussub  13377  ghmsub  13391  dvrcl  13701  unitdvcl  13702  basgen2  14327  opnneiss  14404  cnpf2  14453  sincosq1lem  15071