Theorem syl3an1 859

Description: A syllogism inference.

Hypotheses

Ref	Expression
syl3an.1	|- ((ph /\ ps /\ ch) -> th)
syl3an1.2	|- (ta -> ph)

Assertion

Ref	Expression
syl3an1	|- ((ta /\ ps /\ ch) -> th)

Proof of Theorem syl3an1

Step	Hyp	Ref	Expression
1		syl3an.1	. . . 4 |- ((ph /\ ps /\ ch) -> th)
2	1	3expb 834	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
3		syl3an1.2	. . 3 |- (ta -> ph)
4	2, 3	sylan 448	. 2 |- ((ta /\ (ps /\ ch)) -> th)
5	4	3impb 829	1 |- ((ta /\ ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  syl3an1b 862  syl3an1br 865  syl3anl1 873  wefrc 2943  wereu 2945  tz7.5 2969  f1ofveu 3882  odi 4210  nnmsucr 4240  cnegextlem1 5345  lesub2t 5661  ltsub2t 5663  divnegt 5774  ltdiv2t 5887  supxrunb1 6089  uzwo3lem1 6216  zbtwnre 6221  shftf 6351  peano2uz 6447  seqzcl 6558  expnlbndt 6655  abssubne0t 6882  clim2serzt 7134  caucvglem5 7161  ivthlem6 7286  demoivre 7484  elcls3 7711  mscl 7805  metcl 7811  ssbl 7855  lmss 7953  xpcn 7976  grpcl 8044  grpdivcl 8086  ablmuldiv 8107  abldivdiv4 8109  ablnnncan 8111  ablnnncan1 8113  ringcl 8144  ringgcl 8152  ringcom 8153  ringa4 8156  vccl 8169  vcgcl 8178  vccom 8179  vca4 8182  nvgcl 8239  nvcom 8240  nvadd4 8246  nvscl 8247  nvmval 8263  nvmcl 8267  nmlnoubi 8456  isblo3i 8461  blometi 8463  ipsubdir 8508  hlcom 8602  hlipcj 8613  hlipgt0 8616  psasym 8651  sincosq1sgn 8704  sincosq2sgn 8705  sincosq3sgn 8706  sincosq4sgn 8707  his52t 8954  projlem26 9211  shintcl 9293  chlubt 9432  homco1t 9727  homulasst 9728  adjadjt 9860  homco2t 9901  nmcopexlem5 9955  nmophm 9961  nmcfnexlem5 9984  kbass6t 10054  atcvatlem 10312  mdsymlem3 10332  mdsymlem5 10334  cmppfcd 10703  domcmpc 10704  codcmpc 10705

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain