Theorem a1dd 42

Description: Deduction introducing a nested embedded antecedent. (The proof was shortened by O'Cat, 15-Jan-2008.)

Hypothesis

Ref	Expression
a1dd.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
a1dd	|- (ph -> (ps -> (th -> ch)))

Proof of Theorem a1dd

Step	Hyp	Ref	Expression
1		a1dd.1	. 2 |- (ph -> (ps -> ch))
2		ax-1 4	. 2 |- (ch -> (th -> ch))
3	1, 2	syl6 22	1 |- (ph -> (ps -> (th -> ch)))

Syntax hints:   -> wi 3

This theorem is referenced by:  adantlrr 399  adantrlr 401  adantrrl 402  prlem1 770  a12stdy4 1375  sotri 3443  xpexr 3479  omordi 4197  omwordi 4202  odi 4210  omass 4211  oen0 4213  oewordi 4218  oewordri 4219  axpowndlem3 4951  suppsr2 5223  lemul1it 5837  lemul1itOLD 5838  xrsupsslem 6076  xrinfmsslem 6077  xrub 6080  supxrunb1 6089  supxrunb2 6090  expne0it 6588  expge0t 6591  expwordit 6603  facdivt 6942  facwordit 6944  faclbnd 6945  bccl2t 6971  climconst 7094  climconst2 7095  caucvglem2 7158  ser1clim0 7173  ser1cmp2 7177  isum1p 7206  islp2 7747  bcthlem18 8016  0cnop 9903  0cnfn 9904  dmdbr5at 10349  cmpassoh 10729

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

Copyright terms: Public domain