Theorem syl3an 1139

Description: A triple syllogism inference.

Hypotheses

Ref	Expression
syl3an.1	|- ((ph /\ ps /\ ch) -> th)
syl3an.2	|- (ta -> ph)
syl3an.3	|- (et -> ps)
syl3an.4	|- (ze -> ch)

Assertion

Ref	Expression
syl3an	|- ((ta /\ et /\ ze) -> th)

Proof of Theorem syl3an

Step	Hyp	Ref	Expression
1		syl3an.2	. . 3 |- (ta -> ph)
2		syl3an.3	. . 3 |- (et -> ps)
3		syl3an.4	. . 3 |- (ze -> ch)
4	1, 2, 3	3anim123i 1053	. 2 |- ((ta /\ et /\ ze) -> (ph /\ ps /\ ch))
5		syl3an.1	. 2 |- ((ph /\ ps /\ ch) -> th)
6	4, 5	syl 12	1 |- ((ta /\ et /\ ze) -> th)

Syntax hints:   -> wi 3   /\ w3a 858

This theorem is referenced by:  csbiegft 2573  eloprabg 4936  curry1val 5077  curry2val 5080  nnaord 5290  nnaass 5292  nndi 5293  nnmass 5294  nnacan 5299  nnaword 5300  nnmord 5304  nneob 5312  abfii4 5654  addasspi 6175  mulasspi 6177  distrpi 6178  mulcanpi 6179  ltapi 6182  cnegexlem2 6500  lesub1 6849  lesub2 6850  ltsub1 6851  ltsub2 6852  lemul1 7011  ltmin 7106  zdivadd 7398  qdivcl 7454  qbtwnre 7459  fldiv2 7498  modmulnn 7510  modcyc2 7517  iooneg 7575  uztrn 7597  uzss 7600  elfzle3 7655  fzen 7664  fzaddel 7672  fzss1 7675  fzss2 7676  fzrev 7689  fzrevral2 7699  fzshftral 7701  fsumrev 8289  fsumshftm 8292  abscncflem 8536  efaddlem14 8613  efsub 8633  subbas 8914  blin 9129  metcnf 9162  tgioolem 9192  xplm 9253  iscms2lem4 9270  gxmodid 9402  issubgi 9431  ablmul 9439  nvcnf 9659  nvcni 9661  nvcni2 9662  lnocoi 9757  ipasslem5 9835  ubthlem12 9883  ubthlem12OLD 9884  spwval2 9996  efifolem4 10079  flimfnei 10319  hhssnv 10767  shscli 10914  shmodsi 10995  lnopmi 11562  lnopcoi 11565  hmopco 11585  cnlnadjlem2 11638  adjmul 11662  leopmul2i 11706  leoptr 11708  pjimai 11748  mdslle1i 11889  mdslle2i 11890  mdslj1i 11891  mdslj2i 11892  mdslmd1lem1 11897  mdslmd2i 11902  atexch 11953  atcvatlem 11957  irredlem3 11964  sumdmdii 11987  sumdmdlem 11990  cdj3i 12013  bnj1367 13511  cayleylem2 13642  dvdsnegb 13672  muldvds1 13678  muldvds2 13679  dvdscmul 13680  dvdsmulc 13681  dvdscmulr 13682  dvdsmulcr 13683  dvds2add 13685  dvds2sub 13686  dvdstr 13687  divalglem8 13703  divalgb 13707  divalgmod 13709  ndvdsadd 13711  modgcd 13738  mulgcd 13763  absmulgcd 13764  dvdsgcd 13765  injsurinj 14487  1cat 15106  topfne 15500  isfclusf 15625  flfssfcf 15629  fzmul 15790  fzadd2 15791  fzsplit 15792  lpss2 15842  mettrifi2 15848  geomcau 15849  heiborlem16 15970  hlrelat5 17050  atcvr2 17058  atcvr0eq 17064  zaddablxNEW 17141

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 164  df-an 242  df-3an 860

Copyright terms: Public domain