Theorem a1dd 53

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 25	1 |- (ph -> (ps -> (th -> ch)))

Syntax hints:   -> wi 3

This theorem is referenced by:  adantlrr 435  adantrlr 437  adantrrl 438  dedlem0a 834  prlem1OLD 849  meredith 1200  ee323 1280  a12stdy4 1766  sotri 4315  xpexr 4352  omordi 5245  omwordi 5250  odi 5258  omass 5259  oen0 5261  oewordi 5266  oewordri 5267  omsublim 5887  axpowndlem3 6103  suppsr2 6375  lemul1a 7019  lemul1aOLD 7020  xrsupsslem 7285  xrinfmsslem 7286  xrub 7289  supxrunb1 7298  supxrunb2 7299  expge0 7833  expwordi 7848  facdiv 8194  facwordi 8196  faclbnd 8197  bccl2 8223  climconsti 8354  climconst2 8355  caucvglem2 8418  ser1clim0 8433  ser1cmp2i 8437  isum1p 8467  islp2 9023  metequiv 9158  bcthlem18 9294  0cnop 11540  0cnfn 11541  dmdbr5ati 11994  dfon2lem9 13857  merco2 14203  unpde2eg22 14407  preotr2 14576  prltub 14602  multinv 14771  truni3 14851  stoig2b 14906  conttnf 14944  cntrsetlem 14999  dualcat2lem 15129  cmpassoh 15150  idsubfun 15206  cptarc 15242  a1i14 15328  a1i24 15329  a1i34 15330  finsschain 15373  omsublimOLD 15396  compsub 15431  compfipin0 15436  alexsublem2 15438  alexsublem3 15439  topmtcl 15525  fnejoin1 15530  fnejoin2 15531  ist1-3 15543  filcon 15580  fcluscf 15612  filnetlem1 15640  fimax 15746  fisupg 15748  frfi 15771  filbcmb 15776  vd13 16502  vd23 16503  ee03 16609  ee23an 16625  ee32 16627  ee32an 16629  ee123 16631

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

Copyright terms: Public domain