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  4907  moriotass  5918  nnncan1  8290  lediv1  8924  modqval  10450  modqvalr  10451  modqcl  10452  flqpmodeq  10453  modq0  10455  modqge0  10458  modqlt  10459  modqdiffl  10461  modqdifz  10462  modqvalp1  10469  exp3val  10667  bcval4  10878  ccatval3  11030  ccatfv0  11034  ccatval1lsw  11035  ccatval21sw  11036  lswccatn0lsw  11042  dvdsmultr1  12061  dvdssub2  12065  divalglemeuneg  12153  ndvdsadd  12161  grpsubf  13329  grpinvsub  13332  grpnpcan  13342  mulginvcom  13401  mulginvinv  13402  subgsubcl  13439  qussub  13491  ghmsub  13505  dvrcl  13815  unitdvcl  13816  basgen2  14471  opnneiss  14548  cnpf2  14597  sincosq1lem  15215