Theorem syl9r 72

Description: A nested syllogism inference with different antecedents.

Hypotheses

Ref	Expression
syl9r.1	|- (ph -> (ps -> ch))
syl9r.2	|- (th -> (ch -> ta))

Assertion

Ref	Expression
syl9r	|- (th -> (ph -> (ps -> ta)))

Proof of Theorem syl9r

Step	Hyp	Ref	Expression
1		syl9r.1	. . 3 |- (ph -> (ps -> ch))
2		syl9r.2	. . 3 |- (th -> (ch -> ta))
3	1, 2	syl9 71	. 2 |- (ph -> (th -> (ps -> ta)))
4	3	com12 14	1 |- (th -> (ph -> (ps -> ta)))

Syntax hints:   -> wi 3

This theorem is referenced by:  jadOLD2 157  sylan9r 519  hbsb4 1620  oneqmin 3886  fununi 4481  dfimafn 4720  funimass3 4779  isomin 4876  tz7.48lem 5164  sdomen2 5545  trcl 5752  imbi13 5839  indpi 6186  infxpidmlem7 8827  lmcau 9274  vacnlem6 9672  minveclem27 9916  cncomp 10331  lpni 10347  hlimcauii 10739  spansni 11113  dfon2lem6 13854  trclss 13935  axdenselem8 14026  rngsubpos 14636  gaplc 14731  curgrpact 14735  hscptsscld 15434  alexsublem2 15438  alexsublem3 15439  alexsub 15441  connsub 15443  cnconn 15444  2ndc1stc 15477  neibastop1 15518  neibastop2lem1 15519  neibastop2lem3 15521  neibastop2 15523  topjoin 15527  fnejoin1 15530  fnejoin2 15531  ist1-3 15543  filssufillem 15570  limfilcf 15587  fcluscf 15612  fcluscomp 15621  fisupg 15748  absz 15797  fsum00 15820  heiborlem15 15969

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

Copyright terms: Public domain