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 769  a12stdy4 1373  sotri 3435  xpexr 3471  omordi 4187  omwordi 4192  odi 4200  omass 4201  oen0 4203  oewordi 4208  oewordri 4209  axpowndlem3 4931  suppsr2 5203  lemul1it 5801  lemul1itOLD 5802  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  supxrunb1 6044  supxrunb2 6045  expne0it 6527  expge0t 6530  expwordit 6542  facdivt 6887  facwordit 6889  faclbnd 6890  bccl2t 6917  climconst 7039  climconst2 7040  caucvglem2 7102  ser1clim0 7117  ser1cmp2 7121  isum1p 7149  islp2 7697  bcthlem18 7966  0cnop 9842  0cnfn 9843  dmdbr5at 10284  cmpassoh 10609

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

Copyright terms: Public domain