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 76  pm5.75 761  meredith 936  r19.20da 1755  reuss2 2326  dfwe2 2992  ordom 3198  findsg 3214  finds2 3215  tfindsg 3219  tfinds2 3222  tfinds3 3223  eqfnfv 3854  funfvima2 3910  isofrlem 3959  tfr3 3984  tz7.48lem 4013  oaordi 4238  oeordi 4272  nnacl 4287  nnmcl 4288  nnecl 4289  nnacom 4291  nnmsucr 4298  nnmcom 4299  oaabs 4310  nneneq 4577  inf3lem2 4676  inf3lem5 4679  zorn2lem4 4853  zorn2lem5 4854  zorn2lem6 4855  zorn2lem7 4856  prlem934a 5202  suppsr3 5289  nnaddcl 6000  nnmulcl 6001  sup2 6133  uzind2 6291  uzindOLD 6293  uzwo4OLD 6295  monoord 6381  uzaddcl 6475  uzwo 6481  uzwoOLD 6482  fsequb 6549  om2uzlti 6556  seq1rn2 6580  seqzfveq 6643  seqzrn2 6645  expcllem 6664  expeq0 6674  expgt0 6678  expgt1 6681  mulexp 6683  recexp 6684  expadd 6685  expmul 6686  expmwordi 6695  bernneq 6741  cjexp 6907  absexp 6958  ser1absdiflem 7019  facdiv 7032  facwordi 7034  faclbnd 7035  faclbnd4lem4 7041  faclbnd6 7044  fsumspl 7110  fsumadd 7112  fsumcom 7118  fsumrev 7119  fsumcons 7128  fsumcmp 7130  fsumabs 7133  bcxmas 7166  2climnni 7192  2climnn0i 7193  climaddlem3 7206  climmullem8 7217  ser1cmp2i 7267  cvgcmp3ci 7276  cvgratlem1ALT 7337  cvgratlem1 7340  fsum0diaglem2 7347  fsum0diag2 7349  fsum0diag4 7351  ef0lem 7400  efexp 7462  demoivre 7576  tgcl 7713  bcthlem17 8100  bcthlem18 8101  ipasslem1 8574  occllem6 9261  mdslmd1lem1 10336  mdslmd1lem2 10337  findfvcl 10503

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

Copyright terms: Public domain