Theorem syl3an 866

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 819	. 2 |- ((ta /\ et /\ ze) -> (ph /\ ps /\ ch))
5		syl3an.1	. 2 |- ((ph /\ ps /\ ch) -> th)
6	4, 5	syl 10	1 |- ((ta /\ et /\ ze) -> th)

Syntax hints:   -> wi 3   /\ w3a 773

This theorem is referenced by:  csbiegft 2019  tpss 2467  fr3nr 2916  eloprabg 3992  curry1val 4084  nnaord 4219  nnaass 4221  nndi 4222  nnmass 4223  nnacan 4226  nnaword 4227  nnmord 4231  nneob 4239  abfii4 4538  addasspi 4995  mulasspi 4997  distrpi 4998  mulcanpi 4999  ltapi 5002  cnegextlem2 5318  lesub1t 5633  lesub2t 5634  ltsub1t 5635  ltsub2t 5636  ltmint 5871  qbtwnre 6216  uztrn 6360  uzss 6363  elfzle3 6417  fzaddelt 6432  fzss1t 6435  fzss2t 6436  fzrevt 6443  fzrevral2t 6452  fzshftralt 6454  fsumrev 6967  fsumshftm 6970  abscncflem 7209  efaddlem14 7293  efsubt 7313  subbas 7586  blin 7792  metcnf 7823  tgioolem 7853  xplm 7909  iscms2lem4 7926  issubgi 8059  ablmul 8068  nvcnf 8265  nvcni 8266  lnocoi 8352  ipasslem5 8425  ubthlem12 8471  spwval2 8577  efifolem4 8640  circgrpOLD 8658  hhssnv 9054  shscl 9196  shmods 9277  lnopm 9840  lnopco 9843  hmopcot 9863  cnlnadjlem2 9916  adjmult 9939  leopmul2it 9980  pjima 10015  mdslle1 10152  mdslle2 10153  mdslj1 10154  mdslj2 10155  mdslmd1lem1 10160  mdslmd2 10165  atexcht 10216  atcvatlem 10220  irredlem3 10227  sumdmdi 10249  sumdmdlem 10252  cdj3 10273  cayleylem2 10317  1cat 10536

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