Theorem syl3an1 857

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 832	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
3		syl3an1.2	. . 3 |- (ta -> ph)
4	2, 3	sylan 448	. 2 |- ((ta /\ (ps /\ ch)) -> th)
5	4	3impb 827	1 |- ((ta /\ ps /\ ch) -> th)

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

This theorem is referenced by:  syl3an1b 860  syl3an1br 863  syl3anl1 870  wefrc 2933  wereu 2935  tz7.5 2959  f1ofveu 3867  odi 4194  nnmsucr 4224  cnegextlem1 5317  lesub2t 5634  ltsub2t 5636  divnegt 5730  ltdiv2t 5835  ltdiv23t 5840  lediv23t 5841  supxrunb1 6036  uzwo3lem1 6164  zbtwnre 6169  shftf 6288  peano2uz 6379  seqzcl 6490  abssubne0t 6820  clim2serzt 7070  caucvglem5 7097  ivthlem6 7221  ivthlem6OLD 7230  demoivre 7426  elcls3 7652  mscl 7744  metcl 7750  ssbl 7795  lmss 7888  xpcn 7910  grpcl 7978  grpdivcl 8021  ablmuldiv 8044  abldivdiv4 8046  ablnnncan 8048  ablnnncan1 8050  ringcl 8081  ringgcl 8089  ringcom 8090  ringa4 8093  vccl 8106  vcgcl 8115  vccom 8116  vca4 8119  nvgcl 8179  nvcom 8180  nvadd4 8186  nvscl 8187  nvmval 8203  nvmcl 8207  nmlnoubi 8388  isblo3i 8392  blometi 8394  ipsubdir 8439  hlcom 8532  hlipcj 8543  hlipgt0 8546  psasym 8576  sincosq1sgn 8621  sincosq2sgn 8622  sincosq3sgn 8623  sincosq4sgn 8624  his52t 8875  projlem26 9127  shintcl 9208  chlubt 9347  homco1t 9644  homulasst 9645  adjadjt 9776  homco2t 9817  nmcopexlem5 9870  nmophm 9876  nmcfnexlem5 9899  kbass6t 9966  atcvatlem 10220  mdsymlem3 10240  mdsymlem5 10242  cmppfcd 10547  domcmpc 10548  codcmpc 10549

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 775

Copyright terms: Public domain