Theorem syld3an2 1413

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		simp1 1137	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑)
2		syld3an2.1	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3		simp3 1139	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃)
4		syld3an2.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  enfii  9226  domsdomtrfi  9242  nppcan2  11540  nnncan  11544  nnncan2  11546  div11  11950  subdivcomb2  11963  ltdivmul  12143  ledivmul  12144  ltdiv23  12159  lediv23  12160  xrmaxlt  13223  xrltmin  13224  xrmaxle  13225  xrlemin  13226  pfxtrcfv  14731  pfxco  14877  dvdssub2  16338  dvdsgcdb  16582  lcmdvdsb  16650  vdwapun  17012  poslubdg  18459  ipodrsfi  18584  mulginvcom  19117  matinvgcell  22441  mdetrsca2  22610  mdetrlin2  22613  mdetunilem5  22622  decpmatmul  22778  islp3  23154  bddibl  25875  nvpi  30686  nvabs  30691  nmmulg  33967  lineid  36084  oplecon1b  39202  opltcon1b  39206  oldmm2  39219  oldmj2  39223  cmt3N  39252  2llnneN  39411  cvrexchlem  39421  pmod2iN  39851  polcon2N  39921  paddatclN  39951  osumcllem3N  39960  ltrnval1  40136  cdleme48fv  40501  cdlemg33b  40709  trlcolem  40728  cdlemh  40819  cdlemi1  40820  cdlemi2  40821  cdlemi  40822  cdlemk4  40836  cdlemk19u1  40971  cdlemn3  41199  hgmapfval  41888  pell14qrgap  42886  mnringmulrcld  44247  stoweidlem22  46037  stoweidlem26  46041  sigarexp  46874  lindszr  48386  fv2arycl  48569