Theorem a2d 26

Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)

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 7	. 2 |- ( ( ps -> ( ch -> th ) ) -> ( ( ps -> ch ) -> ( ps -> th ) ) )
3	1, 2	syl 14	1 |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  mpdd  41  imim2d  54  imim3i  61  loowoz  102  animpimp2impd  548  cbv1  1722  ralimdaa  2498  reuss2  3356  finds2  4515  ssrel  4627  ssrel2  4629  ssrelrel  4639  funfvima2  5650  tfrlem1  6205  tfrlemi1  6229  tfr1onlemaccex  6245  tfrcllemaccex  6258  tfri3  6264  nneneq  6751  ac6sfi  6792  pitonn  7656  nnaddcl  8740  nnmulcl  8741  zaddcllempos  9091  zaddcllemneg  9093  peano5uzti  9159  uzind2  9163  fzind  9166  zindd  9169  uzaddcl  9381  exfzdc  10017  frec2uzltd  10176  frecuzrdgg  10189  seq3val  10231  seqvalcd  10232  seq3clss  10240  monoord  10249  seq3caopr3  10254  seq3f1olemp  10275  seq3id3  10280  seq3homo  10283  seq3z  10284  ser3ge0  10290  exp3vallem  10294  expcllem  10304  expap0  10323  mulexp  10332  expadd  10335  expmul  10338  leexp2r  10347  leexp1a  10348  bernneq  10412  facdiv  10484  facwordi  10486  faclbnd  10487  faclbnd6  10490  omgadd  10548  seq3coll  10585  cjexp  10665  resqrexlemover  10782  resqrexlemdecn  10784  resqrexlemlo  10785  resqrexlemcalc3  10788  absexp  10851  fsum2d  11204  modfsummod  11227  fsumabs  11234  fsumiun  11246  binom  11253  bcxmas  11258  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  clim2prod  11308  prodfap0  11314  prodfrecap  11315  demoivreALT  11480  dvdsfac  11558  gcdmultiple  11708  rplpwr  11715  nn0seqcvgd  11722  alginv  11728  algcvga  11732  algfx  11733  prmdvdsexp  11826  prmfac1  11830  ennnfoneleminc  11924  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ennnfonelemhom  11928  tgcl  12233  nninfalllemn  13202  nninfsellemdc  13206