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  4480  f1ofveu  6038  fovcdmda  6198  suppvalfng  6440  smoiso  6533  tfrcl  6595  omv  6688  oeiv  6689  nndi  6719  nnmsucr  6721  f1oen2g  6994  f1dom2g  6995  undiffi  7185  prarloclemarch2  7734  distrnq0  7774  ltprordil  7904  1idprl  7905  1idpru  7906  ltpopr  7910  ltexprlemopu  7918  ltexprlemdisj  7921  ltexprlemfl  7924  ltexprlemfu  7926  ltexprlemru  7927  recexprlemdisj  7945  recexprlemss1l  7950  recexprlemss1u  7951  cnegexlem1  8448  msqge0  8890  mulge0  8893  divnegap  8980  divdiv32ap  8994  divneg2ap  9010  peano2uz  9915  lbzbi  9948  negqmod0  10693  modqmuladdnn0  10730  expnlbnd  11026  fun2dmnop  11223  shftfvalg  11503  xrmaxaddlem  11945  retanclap  12408  tannegap  12414  demoivreALT  12460  gcd0id  12675  isprm3  12815  euclemma  12843  phiprmpw  12919  fermltl  12931  sgrpcl  13622  mndcl  13636  imasmnd2  13665  grpcl  13721  dfgrp2  13740  grprcan  13750  grpsubcl  13793  imasgrp2  13827  mhmid  13832  mhmmnd  13833  mulginvcom  13864  mulgnndir  13868  mulgnnass  13874  qusgrp  13949  ghmmulg  13973  ghmrn  13974  ghmeqker  13988  ablcom  14020  ablinvadd  14027  ghmcmn  14044  rngacl  14086  rngpropd  14099  srgacl  14126  srgcom  14127  ringacl  14174  imasring  14208  subrngacl  14353  subrgacl  14377  subrgugrp  14385  lmodacl  14447  lmodmcl  14448  lmodvacl  14450  lmodvsubcl  14480  lmod4  14485  lmodvaddsub4  14487  lmodvpncan  14488  lmodvnpcan  14489  lmodsubeq0  14494  psmetcl  15191  xmetcl  15217  metcl  15218  meteq0  15225  metge0  15231  metsym  15236  blelrnps  15284  blelrn  15285  blssm  15286  blres  15299  mscl  15330  xmscl  15331  xmsge0  15332  xmseq0  15333  xmssym  15334  mopnin  15352  sincosq1sgn  15691  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  lgsneg1  15898  usgredg2vtx  16212  uspgredg2vtxeu  16213  usgredg2vtxeu  16214