Theorem syld3an2 1414

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 1374	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  9122  domsdomtrfi  9138  nppcan2  11424  nnncan  11428  nnncan2  11430  div11  11836  subdivcomb2  11849  ltdivmul  12029  ledivmul  12030  ltdiv23  12045  lediv23  12046  xrmaxlt  13108  xrltmin  13109  xrmaxle  13110  xrlemin  13111  pfxtrcfv  14628  pfxco  14773  dvdssub2  16240  dvdsgcdb  16484  lcmdvdsb  16552  vdwapun  16914  poslubdg  18347  ipodrsfi  18474  mulginvcom  19041  matinvgcell  22391  mdetrsca2  22560  mdetrlin2  22563  mdetunilem5  22572  decpmatmul  22728  islp3  23102  bddibl  25809  nvpi  30755  nvabs  30760  nmmulg  34144  fineqvnttrclselem2  35300  fineqvnttrclselem3  35301  lineid  36299  oplecon1b  39577  opltcon1b  39581  oldmm2  39594  oldmj2  39598  cmt3N  39627  2llnneN  39785  cvrexchlem  39795  pmod2iN  40225  polcon2N  40295  paddatclN  40325  osumcllem3N  40334  ltrnval1  40510  cdleme48fv  40875  cdlemg33b  41083  trlcolem  41102  cdlemh  41193  cdlemi1  41194  cdlemi2  41195  cdlemi  41196  cdlemk4  41210  cdlemk19u1  41345  cdlemn3  41573  hgmapfval  42262  pell14qrgap  43232  mnringmulrcld  44584  stoweidlem22  46380  stoweidlem26  46384  sigarexp  47217  lindszr  48829  fv2arycl  49008