Theorem expr 375

Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

Ref	Expression
expr.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
expr	|- ( ( ph /\ ps ) -> ( ch -> th ) )

Proof of Theorem expr

Step	Hyp	Ref	Expression
1		expr.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	exp32 365	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 124	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  animpimp2impd  565  reximddv  2653  rexlimdvaa  2669  issod  4466  ordsuc  4712  fcof1  5992  riota5f  6068  ovmpodf  6223  suppssdc  6504  tfrlemi1  6608  eqsuptid  7344  eqinftid  7368  ordiso2  7382  addnq0mo  7821  mulnq0mo  7822  genprndl  7895  genprndu  7896  addlocpr  7910  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemfl  7983  ltexprlemfu  7985  aptiprleml  8013  caucvgprprlemexbt  8080  addsrmo  8117  mulsrmo  8118  prodge0  9193  un0addcl  9608  un0mulcl  9609  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  monoord  10943  seq3split  10946  seqsplitg  10947  seqf1oglem1  10977  seq3id2  10984  seqhomog  10988  expnegzap  11031  expcanlem  11175  bcval5  11223  hashfibc  11305  seq3coll  11316  wrdind  11516  wrd2ind  11517  caucvgrelemcau  11768  cau3lem  11903  reccn2ap  12104  summodclem2  12174  zsumdc  12176  fsumf1o  12182  fisumss  12184  fsumcl2lem  12190  fsumadd  12198  fisum0diag2  12239  fsummulc2  12240  mertenslem2  12328  prodmodclem2  12369  zproddc  12371  fprodseq  12375  fprodf1o  12380  prodssdc  12381  fprodssdc  12382  fprodmul  12383  dvds0lem  12593  dvdsnegb  12600  dvdssub2  12627  isprm6  12951  hashgcdeq  13047  modprminv  13057  modprminveq  13058  reumodprminv  13061  pcqmul  13111  pcqcl  13114  pcxnn0cl  13118  pcxcl  13119  pc2dvds  13138  pcadd  13148  pcmpt  13151  pockthg  13165  infpnlem1  13167  ballotfilemfc0  13290  ballotfilemfcc  13291  mgmidsssn0  13763  mhmeql  13858  grprcan  13901  dfgrp3mlem  13962  mulgnn0ass  14020  isnsg3  14069  ghmpreima  14128  ghmeql  14129  lss1d  14829  znidomb  15102  rnasclassa  15147  mvrf1fi  15231  topssnei  15421  innei  15422  cnptopco  15481  cncnpi  15487  cncnp  15489  cnconst2  15492  cnpdis  15501  lmtopcnp  15509  tx2cn  15529  txdis  15536  blssps  15686  blss  15687  neibl  15750  metss  15753  metequiv2  15755  metrest  15765  metcnp3  15770  ivthinclemlopn  15895  ivthinclemlr  15896  ivthinclemuopn  15897  ivthinclemur  15898  ivthinclemloc  15900  plycolemc  16017  rpcxpmul2z  16181  ppinprm  16293  chtnprm  16295  mpodvdsmulf1o  16317  chtublem  16328  perfectlem2  16333  bposlem1  16344  bposlem3  16346  2sqlem5  16476  2sqlem6  16477  2sqlem8  16480  2sqlem10  16482  nconstwlpolem  17355