Theorem syld3an2 1373

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

Ref	Expression
syld3an2.1	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
syld3an2.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syld3an2	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Proof of Theorem syld3an2

Step	Hyp	Ref	Expression
1		syld3an2.1	. . . 4 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3com23 1271	. . 3 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜒) → 𝜓)
3		syld3an2.2	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
4	3	3com23 1271	. . 3 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜏)
5	2, 4	syld3an3 1371	. 2 ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜒) → 𝜏)
6	5	3com23 1271	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  nppcan2  10312  nnncan  10316  nnncan2  10318  ltdivmul  10898  ledivmul  10899  ltdiv23  10914  lediv23  10915  xrmaxlt  12012  xrltmin  12013  xrmaxle  12014  xrlemin  12015  swrdtrcfv  13441  dvdssub2  15023  dvdsgcdb  15262  lcmdvdsb  15326  vdwapun  15678  poslubdg  17149  ipodrsfi  17163  mulginvcom  17565  matinvgcell  20241  mdetrsca2  20410  mdetrlin2  20413  mdetunilem5  20422  decpmatmul  20577  islp3  20950  bddibl  23606  nvpi  27522  nvabs  27527  nmmulg  30012  subdivcomb2  31612  lineid  32190  oplecon1b  34488  opltcon1b  34492  oldmm2  34505  oldmj2  34509  cmt3N  34538  2llnneN  34695  cvrexchlem  34705  pmod2iN  35135  polcon2N  35205  paddatclN  35235  osumcllem3N  35244  ltrnval1  35420  cdleme48fv  35787  cdlemg33b  35995  trlcolem  36014  cdlemh  36105  cdlemi1  36106  cdlemi2  36107  cdlemi  36108  cdlemk4  36122  cdlemk19u1  36257  cdlemn3  36486  hgmapfval  37178  pell14qrgap  37439  stoweidlem22  40239  stoweidlem26  40243  sigarexp  41048  pfxtrcfv  41401  pfxco  41438  lindszr  42258