Theorem syl3an 867

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 820	. 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 774

This theorem is referenced by:  csbiegft 2026  tpss 2473  fr3nr 2922  eloprabg 4002  curry1val 4093  nnaord 4228  nnaass 4230  nndi 4231  nnmass 4232  nnacan 4235  nnaword 4236  nnmord 4240  nneob 4248  abfii4 4547  addasspi 5006  mulasspi 5008  distrpi 5009  mulcanpi 5010  ltapi 5013  cnegextlem2 5329  lesub1t 5643  lesub2t 5644  ltsub1t 5645  ltsub2t 5646  ltmint 5881  qbtwnre 6228  uztrn 6373  uzss 6376  elfzle3 6430  fzaddelt 6445  fzss1t 6448  fzss2t 6449  fzrevt 6456  fzrevral2t 6465  fzshftralt 6467  fsumrev 6982  fsumshftm 6985  abscncflem 7226  efaddlem14 7310  efsubt 7330  subbas 7604  blin 7814  metcnf 7846  tgioolem 7876  xplm 7937  iscms2lem4 7954  issubgi 8086  ablmul 8095  nvcnf 8291  nvcni 8293  nvcni2 8294  lnocoi 8380  ipasslem5 8453  ubthlem12 8499  spwval2 8610  efifolem4 8675  circgrpOLD 8693  hhssnv 9089  shscl 9236  shmods 9317  lnopm 9881  lnopco 9884  hmopcot 9904  cnlnadjlem2 9957  adjmult 9981  leopmul2it 10024  leoptrt 10026  pjima 10060  mdslle1 10200  mdslle2 10201  mdslj1 10202  mdslj2 10203  mdslmd1lem1 10208  mdslmd2 10213  atexcht 10264  atcvatlem 10268  irredlem3 10275  sumdmdi 10298  sumdmdlem 10301  cdj3 10324  cayleylem2 10366  1cat 10608

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 776

Copyright terms: Public domain