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  559  reximddv  2633  rexlimdvaa  2649  issod  4410  ordsuc  4655  fcof1  5913  riota5f  5987  ovmpodf  6142  tfrlemi1  6484  eqsuptid  7172  eqinftid  7196  ordiso2  7210  addnq0mo  7642  mulnq0mo  7643  genprndl  7716  genprndu  7717  addlocpr  7731  ltexprlemm  7795  ltexprlemopl  7796  ltexprlemopu  7798  ltexprlemfl  7804  ltexprlemfu  7806  aptiprleml  7834  caucvgprprlemexbt  7901  addsrmo  7938  mulsrmo  7939  prodge0  9009  un0addcl  9410  un0mulcl  9411  seq3fveq2  10705  seqfveq2g  10707  seq3shft2  10711  seqshft2g  10712  monoord  10715  seq3split  10718  seqsplitg  10719  seqf1oglem1  10749  seq3id2  10756  seqhomog  10760  expnegzap  10803  expcanlem  10945  bcval5  10993  seq3coll  11072  wrdind  11262  wrd2ind  11263  caucvgrelemcau  11499  cau3lem  11633  reccn2ap  11832  summodclem2  11901  zsumdc  11903  fsumf1o  11909  fisumss  11911  fsumcl2lem  11917  fsumadd  11925  fisum0diag2  11966  fsummulc2  11967  mertenslem2  12055  prodmodclem2  12096  zproddc  12098  fprodseq  12102  fprodf1o  12107  prodssdc  12108  fprodssdc  12109  fprodmul  12110  dvds0lem  12320  dvdsnegb  12327  dvdssub2  12354  isprm6  12677  hashgcdeq  12770  modprminv  12780  modprminveq  12781  reumodprminv  12784  pcqmul  12834  pcqcl  12837  pcxnn0cl  12841  pcxcl  12842  pc2dvds  12861  pcadd  12871  pcmpt  12874  pockthg  12888  infpnlem1  12890  mgmidsssn0  13425  mhmeql  13533  grprcan  13578  dfgrp3mlem  13639  mulgnn0ass  13703  isnsg3  13752  ghmpreima  13811  ghmeql  13812  lss1d  14355  znidomb  14630  topssnei  14844  innei  14845  cnptopco  14904  cncnpi  14910  cncnp  14912  cnconst2  14915  cnpdis  14924  lmtopcnp  14932  tx2cn  14952  txdis  14959  blssps  15109  blss  15110  neibl  15173  metss  15176  metequiv2  15178  metrest  15188  metcnp3  15193  ivthinclemlopn  15318  ivthinclemlr  15319  ivthinclemuopn  15320  ivthinclemur  15321  ivthinclemloc  15323  plycolemc  15440  mpodvdsmulf1o  15672  perfectlem2  15682  2sqlem5  15806  2sqlem6  15807  2sqlem8  15810  2sqlem10  15812  nconstwlpolem  16463