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  561  reximddv  2636  rexlimdvaa  2652  issod  4422  ordsuc  4667  fcof1  5934  riota5f  6008  ovmpodf  6163  suppssdc  6438  tfrlemi1  6541  eqsuptid  7239  eqinftid  7263  ordiso2  7277  addnq0mo  7710  mulnq0mo  7711  genprndl  7784  genprndu  7785  addlocpr  7799  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemfl  7872  ltexprlemfu  7874  aptiprleml  7902  caucvgprprlemexbt  7969  addsrmo  8006  mulsrmo  8007  prodge0  9077  un0addcl  9478  un0mulcl  9479  seq3fveq2  10781  seqfveq2g  10783  seq3shft2  10787  seqshft2g  10788  monoord  10791  seq3split  10794  seqsplitg  10795  seqf1oglem1  10825  seq3id2  10832  seqhomog  10836  expnegzap  10879  expcanlem  11021  bcval5  11069  seq3coll  11150  wrdind  11350  wrd2ind  11351  caucvgrelemcau  11601  cau3lem  11735  reccn2ap  11934  summodclem2  12004  zsumdc  12006  fsumf1o  12012  fisumss  12014  fsumcl2lem  12020  fsumadd  12028  fisum0diag2  12069  fsummulc2  12070  mertenslem2  12158  prodmodclem2  12199  zproddc  12201  fprodseq  12205  fprodf1o  12210  prodssdc  12211  fprodssdc  12212  fprodmul  12213  dvds0lem  12423  dvdsnegb  12430  dvdssub2  12457  isprm6  12780  hashgcdeq  12873  modprminv  12883  modprminveq  12884  reumodprminv  12887  pcqmul  12937  pcqcl  12940  pcxnn0cl  12944  pcxcl  12945  pc2dvds  12964  pcadd  12974  pcmpt  12977  pockthg  12991  infpnlem1  12993  mgmidsssn0  13528  mhmeql  13636  grprcan  13681  dfgrp3mlem  13742  mulgnn0ass  13806  isnsg3  13855  ghmpreima  13914  ghmeql  13915  lss1d  14459  znidomb  14734  topssnei  14953  innei  14954  cnptopco  15013  cncnpi  15019  cncnp  15021  cnconst2  15024  cnpdis  15033  lmtopcnp  15041  tx2cn  15061  txdis  15068  blssps  15218  blss  15219  neibl  15282  metss  15285  metequiv2  15287  metrest  15297  metcnp3  15302  ivthinclemlopn  15427  ivthinclemlr  15428  ivthinclemuopn  15429  ivthinclemur  15430  ivthinclemloc  15432  plycolemc  15549  mpodvdsmulf1o  15784  perfectlem2  15794  2sqlem5  15918  2sqlem6  15919  2sqlem8  15922  2sqlem10  15924  nconstwlpolem  16778