Theorem syl3an1 1307

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

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

Assertion

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

Proof of Theorem syl3an1

Step	Hyp	Ref	Expression
1		syl3an1.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	3anim1i 1212	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an1.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 14	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  syl3an1b  1310  syl3an1br  1313  wepo  4462  f1ofveu  6016  fovcdmda  6176  suppvalfng  6418  smoiso  6511  tfrcl  6573  omv  6666  oeiv  6667  nndi  6697  nnmsucr  6699  f1oen2g  6971  f1dom2g  6972  undiffi  7160  prarloclemarch2  7682  distrnq0  7722  ltprordil  7852  1idprl  7853  1idpru  7854  ltpopr  7858  ltexprlemopu  7866  ltexprlemdisj  7869  ltexprlemfl  7872  ltexprlemfu  7874  ltexprlemru  7875  recexprlemdisj  7893  recexprlemss1l  7898  recexprlemss1u  7899  cnegexlem1  8396  msqge0  8838  mulge0  8841  divnegap  8928  divdiv32ap  8942  divneg2ap  8958  peano2uz  9861  lbzbi  9894  negqmod0  10639  modqmuladdnn0  10676  expnlbnd  10972  fun2dmnop  11161  shftfvalg  11441  xrmaxaddlem  11883  retanclap  12346  tannegap  12352  demoivreALT  12398  gcd0id  12613  isprm3  12753  euclemma  12781  phiprmpw  12857  fermltl  12869  sgrpcl  13555  mndcl  13569  imasmnd2  13598  grpcl  13654  dfgrp2  13673  grprcan  13683  grpsubcl  13726  imasgrp2  13760  mhmid  13765  mhmmnd  13766  mulginvcom  13797  mulgnndir  13801  mulgnnass  13807  qusgrp  13882  ghmmulg  13906  ghmrn  13907  ghmeqker  13921  ablcom  13953  ablinvadd  13960  ghmcmn  13977  rngacl  14019  rngpropd  14032  srgacl  14059  srgcom  14060  ringacl  14107  imasring  14141  subrngacl  14286  subrgacl  14310  subrgugrp  14318  lmodacl  14378  lmodmcl  14379  lmodvacl  14381  lmodvsubcl  14411  lmod4  14416  lmodvaddsub4  14418  lmodvpncan  14419  lmodvnpcan  14420  lmodsubeq0  14425  psmetcl  15120  xmetcl  15146  metcl  15147  meteq0  15154  metge0  15160  metsym  15165  blelrnps  15213  blelrn  15214  blssm  15215  blres  15228  mscl  15259  xmscl  15260  xmsge0  15261  xmseq0  15262  xmssym  15263  mopnin  15281  sincosq1sgn  15620  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  lgsneg1  15827  usgredg2vtx  16141  uspgredg2vtxeu  16142  usgredg2vtxeu  16143