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 ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  animpimp2impd  565  reximddv  2653  rexlimdvaa  2669  issod  4462  ordsuc  4708  fcof1  5983  riota5f  6059  ovmpodf  6214  suppssdc  6494  tfrlemi1  6597  eqsuptid  7331  eqinftid  7355  ordiso2  7369  addnq0mo  7808  mulnq0mo  7809  genprndl  7882  genprndu  7883  addlocpr  7897  ltexprlemm  7961  ltexprlemopl  7962  ltexprlemopu  7964  ltexprlemfl  7970  ltexprlemfu  7972  aptiprleml  8000  caucvgprprlemexbt  8067  addsrmo  8104  mulsrmo  8105  prodge0  9178  un0addcl  9579  un0mulcl  9580  seq3fveq2  10895  seqfveq2g  10897  seq3shft2  10901  seqshft2g  10902  monoord  10905  seq3split  10908  seqsplitg  10909  seqf1oglem1  10939  seq3id2  10946  seqhomog  10950  expnegzap  10993  expcanlem  11136  bcval5  11184  hashfibc  11266  seq3coll  11277  wrdind  11477  wrd2ind  11478  caucvgrelemcau  11729  cau3lem  11863  reccn2ap  12062  summodclem2  12132  zsumdc  12134  fsumf1o  12140  fisumss  12142  fsumcl2lem  12148  fsumadd  12156  fisum0diag2  12197  fsummulc2  12198  mertenslem2  12286  prodmodclem2  12327  zproddc  12329  fprodseq  12333  fprodf1o  12338  prodssdc  12339  fprodssdc  12340  fprodmul  12341  dvds0lem  12551  dvdsnegb  12558  dvdssub2  12585  isprm6  12908  hashgcdeq  13001  modprminv  13011  modprminveq  13012  reumodprminv  13015  pcqmul  13065  pcqcl  13068  pcxnn0cl  13072  pcxcl  13073  pc2dvds  13092  pcadd  13102  pcmpt  13105  pockthg  13119  infpnlem1  13121  ballotfilemfc0  13215  ballotfilemfcc  13216  mgmidsssn0  13687  mhmeql  13782  grprcan  13825  dfgrp3mlem  13886  mulgnn0ass  13944  isnsg3  13993  ghmpreima  14052  ghmeql  14053  lss1d  14703  znidomb  14976  rnasclassa  15021  topssnei  15246  innei  15247  cnptopco  15306  cncnpi  15312  cncnp  15314  cnconst2  15317  cnpdis  15326  lmtopcnp  15334  tx2cn  15354  txdis  15361  blssps  15511  blss  15512  neibl  15575  metss  15578  metequiv2  15580  metrest  15590  metcnp3  15595  ivthinclemlopn  15720  ivthinclemlr  15721  ivthinclemuopn  15722  ivthinclemur  15723  ivthinclemloc  15725  plycolemc  15842  mpodvdsmulf1o  16087  perfectlem2  16097  2sqlem5  16221  2sqlem6  16222  2sqlem8  16225  2sqlem10  16227  nconstwlpolem  17089