Theorem sylsyld 32

Description: Virtual deduction rule e12 16593 without virtual deduction symbols. (Contributed by Alan Sare, 20-Apr-2011.)

Hypotheses

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

Assertion

Ref	Expression
sylsyld	|- (ph -> (ch -> ta))

Proof of Theorem sylsyld

Step	Hyp	Ref	Expression
1		ee12.2	. 2 |- (ph -> (ch -> th))
2		ee12.1	. . 3 |- (ph -> ps)
3		ee12.3	. . 3 |- (ps -> (th -> ta))
4	2, 3	syl 12	. 2 |- (ph -> (th -> ta))
5	1, 4	syld 30	1 |- (ph -> (ch -> ta))

Syntax hints:   -> wi 3

This theorem is referenced by:  3ornot23 1281  ax10o 1499  sbiedOLD 1564  a16g 1653  a16gOLD 1654  ralcom2 2244  el 3485  onfununi 5116  tfrlem2 5120  unfi 5644  tratrb 5831  cardaleph 6033  ordpipq 6208  distrlem4pr 6282  ltsrpr 6338  climaddlem3 8376  climmullem8 8387  caucvglem6 8422  cncnplem4 9054  cmsss 9275  fbunfip 10282  occon2 10794  atexch 11953  frmin 13938  ufcomp 15622  findcard2 15745  mettrifi 15847  totbndbnd 15944  rrntotbnd 16022  trint0 16439  smoiun 16452  trsspwALT2 16641  sspwtrALT 16644

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

Copyright terms: Public domain