Theorem syld3an3 1318

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  syld3an1  1319  syld3an2  1320  brelrng  4963  moriotass  6002  nnncan1  8415  lediv1  9049  modqval  10587  modqvalr  10588  modqcl  10589  flqpmodeq  10590  modq0  10592  modqge0  10595  modqlt  10596  modqdiffl  10598  modqdifz  10599  modqvalp1  10606  exp3val  10804  bcval4  11015  ccatval3  11180  ccatfv0  11184  ccatval1lsw  11185  ccatval21sw  11186  lswccatn0lsw  11192  pfxsuff1eqwrdeq  11284  pfxccatid  11326  dvdsmultr1  12410  dvdssub2  12414  divalglemeuneg  12502  ndvdsadd  12510  grpsubf  13680  grpinvsub  13683  grpnpcan  13693  mulginvcom  13752  mulginvinv  13753  subgsubcl  13790  qussub  13842  ghmsub  13856  dvrcl  14168  unitdvcl  14169  basgen2  14824  opnneiss  14901  cnpf2  14950  sincosq1lem  15568