Theorem a2d 13

Description: Deduction distributing an embedded antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem a2d

Step	Hyp	Ref	Expression
1		a2d.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		ax-2 5	. 2 |- ((ps -> (ch -> th)) -> ((ps -> ch) -> (ps -> th)))
3	1, 2	syl 10	1 |- (ph -> ((ps -> ch) -> (ps -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  imim2 14  imim3i 19  imim2d 25  mpdd 46  loowoz 73  pm5.75 747  meredith 921  r19.20da 1700  reuss2 2265  dfwe2 2925  ordom 3131  findsg 3147  finds2 3148  tfindsg 3152  tfinds2 3155  tfinds3 3156  eqfnfv 3782  funfvima2 3838  isofrlem 3886  tfr3 3911  tz7.48lem 3940  oaordi 4164  oeordi 4198  nnacl 4213  nnmcl 4214  nnecl 4215  nnacom 4217  nnmsucr 4224  nnmcom 4225  oaabs 4236  nneneq 4492  inf3lem2 4586  inf3lem5 4589  zorn2lem4 4763  zorn2lem5 4764  zorn2lem6 4765  zorn2lem7 4766  prlem934a 5109  suppsr3 5196  nnaddclt 5888  nnmulclt 5889  sup2 5998  uzind2 6154  uzindOLD 6156  uzwo4OLD 6158  monoord 6231  om2uzlt 6235  seq1rn2 6258  uzaddclt 6381  uzwo 6387  uzwoOLD 6388  fsequb 6455  seqzfveq 6486  seqzrn2 6488  expcllem 6507  expeq0t 6517  expgt0t 6520  expgt1t 6523  mulexpt 6525  recexpt 6526  expaddt 6527  expmult 6528  expmwordit 6537  bernneq 6583  cjexpt 6752  absexpt 6803  ser1absdiflem 6866  facdivt 6879  facwordit 6881  faclbnd 6882  faclbnd4lem4 6888  faclbnd6 6891  fsumsplit 6958  fsumadd 6960  fsumcom 6966  fsumrev 6967  fsumconst 6976  fsumcmp 6978  fsumabs 6981  bcxmas 7014  2climnn 7039  2climnn0 7040  climaddlem3 7052  climmullem8 7063  ser1cmp2 7113  cvgcmp3c 7122  cvgratlem1ALT 7182  cvgratlem1 7185  fsum0diaglem2 7192  fsum0diag2 7194  fsum0diag4 7196  ef0lem 7252  efexpt 7314  demoivre 7426  tgclt 7566  bcthlem17 7949  bcthlem18 7950  ipasslem1 8421  occllem6 9094  mdslmd1lem1 10160  mdslmd1lem2 10161  findfvcl 10323

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

Copyright terms: Public domain