Theorem syl3an1 1282

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 1187	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an1.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 14	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  syl3an1b  1285  syl3an1br  1288  wepo  4374  f1ofveu  5880  fovcdmda  6036  smoiso  6322  tfrcl  6384  omv  6475  oeiv  6476  nndi  6506  nnmsucr  6508  f1oen2g  6776  f1dom2g  6777  undiffi  6948  prarloclemarch2  7443  distrnq0  7483  ltprordil  7613  1idprl  7614  1idpru  7615  ltpopr  7619  ltexprlemopu  7627  ltexprlemdisj  7630  ltexprlemfl  7633  ltexprlemfu  7635  ltexprlemru  7636  recexprlemdisj  7654  recexprlemss1l  7659  recexprlemss1u  7660  cnegexlem1  8157  msqge0  8598  mulge0  8601  divnegap  8688  divdiv32ap  8702  divneg2ap  8718  peano2uz  9608  lbzbi  9641  negqmod0  10357  modqmuladdnn0  10394  expnlbnd  10671  shftfvalg  10854  xrmaxaddlem  11295  retanclap  11757  tannegap  11763  demoivreALT  11808  gcd0id  12007  isprm3  12145  euclemma  12173  phiprmpw  12249  fermltl  12261  sgrpcl  12865  mndcl  12877  grpcl  12946  dfgrp2  12964  grprcan  12974  grpsubcl  13017  imasgrp2  13045  mhmid  13050  mhmmnd  13051  mulginvcom  13080  mulgnndir  13084  mulgnnass  13090  qusgrp  13164  ghmmulg  13188  ghmrn  13189  ghmeqker  13203  ablcom  13235  ablinvadd  13242  ghmcmn  13258  rngacl  13289  rngpropd  13302  srgacl  13329  srgcom  13330  ringacl  13377  imasring  13407  subrngacl  13548  subrgacl  13572  subrgugrp  13580  lmodacl  13608  lmodmcl  13609  lmodvacl  13611  lmodvsubcl  13641  lmod4  13646  lmodvaddsub4  13648  lmodvpncan  13649  lmodvnpcan  13650  lmodsubeq0  13655  psmetcl  14263  xmetcl  14289  metcl  14290  meteq0  14297  metge0  14303  metsym  14308  blelrnps  14356  blelrn  14357  blssm  14358  blres  14371  mscl  14402  xmscl  14403  xmsge0  14404  xmseq0  14405  xmssym  14406  mopnin  14424  sincosq1sgn  14684  sincosq2sgn  14685  sincosq3sgn  14686  sincosq4sgn  14687  lgsneg1  14864