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 754  meredith 931  r19.20da 1754  reuss2 2327  dfwe2 3140  tfindsg 3213  tfinds2 3216  tfinds3 3217  ordom 3228  findsg 3245  finds2 3246  eqfnfv 3909  eqfnfv2 3911  funfvima2 3967  isofrlem 4015  tfr3 4227  tz7.48lem 4256  oaordi 4316  oeordi 4350  nnacl 4369  nnmcl 4370  nnecl 4371  nnacom 4373  nnmsucr 4380  nnmcom 4381  oaabs 4392  nneneq 4659  inf3lem2 4759  inf3lem5 4762  zorn2lem4 4937  zorn2lem5 4938  zorn2lem6 4939  zorn2lem7 4940  prlem934a 5291  suppsr3 5378  nnaddcl 6085  nnmulcl 6086  sup2 6219  uzind2 6377  uzindOLD 6379  uzwo4OLD 6381  zindd 6386  monoord 6482  uzaddcl 6576  uzwo 6582  uzwoOLD 6583  fsequb 6654  om2uzlti 6661  seq1rn2 6686  seqzfveq 6749  seqzrn2 6751  expcllem 6770  expeq0 6780  expgt0 6783  expgt1 6786  mulexp 6788  exprec 6789  exprecOLD 6790  expadd 6791  expmul 6792  expmwordi 6803  bernneq 6849  bernneqOLD 6850  cjexp 7018  absexp 7070  ser1absdiflem 7132  facdiv 7145  facwordi 7147  faclbnd 7148  faclbnd4lem4 7154  faclbnd6 7157  fsumsplit 7223  fsumadd 7225  fsumcom 7231  fsumrev 7232  fsumconst 7241  fsumcmp 7243  fsumabs 7246  bcxmas 7279  2climnn 7305  2climnn0 7306  climaddlem3 7319  climmullem8 7330  ser1cmp2i 7380  cvgcmp3ci 7390  cvgratlem1ALT 7452  cvgratlem1 7455  fsum0diaglem2 7462  fsum0diag2 7464  fsum0diag4 7466  ef0lem 7515  efexp 7577  demoivre 7695  tgcl 7836  bcthlem17 8226  bcthlem18 8227  gxnn0add 8330  gxnn0mul 8333  ipasslem1 8746  occllem6 9454  mdslmd1lem1 10533  mdslmd1lem2 10534  findfvcl 10701  fictb 11423  ordtypelem4 11430  ordtypelem7 11433  neibastop2lem1 11580  flimfcls 11725  sdclem1 11875  sdclem2 11876  seqpo 11878  incsequz 11879  fsum00 11883  fsumlt 11884  mettrifi 11912  lmtlm 11969

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

Copyright terms: Public domain