Theorem syld3an3 1316

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  syld3an1  1317  syld3an2  1318  brelrng  4955  moriotass  5991  nnncan1  8393  lediv1  9027  modqval  10558  modqvalr  10559  modqcl  10560  flqpmodeq  10561  modq0  10563  modqge0  10566  modqlt  10567  modqdiffl  10569  modqdifz  10570  modqvalp1  10577  exp3val  10775  bcval4  10986  ccatval3  11147  ccatfv0  11151  ccatval1lsw  11152  ccatval21sw  11153  lswccatn0lsw  11159  pfxsuff1eqwrdeq  11246  pfxccatid  11288  dvdsmultr1  12357  dvdssub2  12361  divalglemeuneg  12449  ndvdsadd  12457  grpsubf  13627  grpinvsub  13630  grpnpcan  13640  mulginvcom  13699  mulginvinv  13700  subgsubcl  13737  qussub  13789  ghmsub  13803  dvrcl  14114  unitdvcl  14115  basgen2  14770  opnneiss  14847  cnpf2  14896  sincosq1lem  15514