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  2647  rexlimdvaa  2663  issod  4445  ordsuc  4690  fcof1  5962  riota5f  6038  ovmpodf  6193  suppssdc  6473  tfrlemi1  6576  eqsuptid  7301  eqinftid  7325  ordiso2  7339  addnq0mo  7778  mulnq0mo  7779  genprndl  7852  genprndu  7853  addlocpr  7867  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemfl  7940  ltexprlemfu  7942  aptiprleml  7970  caucvgprprlemexbt  8037  addsrmo  8074  mulsrmo  8075  prodge0  9145  un0addcl  9546  un0mulcl  9547  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord  10871  seq3split  10874  seqsplitg  10875  seqf1oglem1  10905  seq3id2  10912  seqhomog  10916  expnegzap  10959  expcanlem  11102  bcval5  11150  hashfibc  11232  seq3coll  11239  wrdind  11439  wrd2ind  11440  caucvgrelemcau  11690  cau3lem  11824  reccn2ap  12023  summodclem2  12093  zsumdc  12095  fsumf1o  12101  fisumss  12103  fsumcl2lem  12109  fsumadd  12117  fisum0diag2  12158  fsummulc2  12159  mertenslem2  12247  prodmodclem2  12288  zproddc  12290  fprodseq  12294  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodmul  12302  dvds0lem  12512  dvdsnegb  12519  dvdssub2  12546  isprm6  12869  hashgcdeq  12962  modprminv  12972  modprminveq  12973  reumodprminv  12976  pcqmul  13026  pcqcl  13029  pcxnn0cl  13033  pcxcl  13034  pc2dvds  13053  pcadd  13063  pcmpt  13066  pockthg  13080  infpnlem1  13082  ballotfilemfc0  13176  ballotfilemfcc  13177  mgmidsssn0  13681  mhmeql  13789  grprcan  13834  dfgrp3mlem  13895  mulgnn0ass  13959  isnsg3  14008  ghmpreima  14067  ghmeql  14068  lss1d  14643  znidomb  14918  topssnei  15139  innei  15140  cnptopco  15199  cncnpi  15205  cncnp  15207  cnconst2  15210  cnpdis  15219  lmtopcnp  15227  tx2cn  15247  txdis  15254  blssps  15404  blss  15405  neibl  15468  metss  15471  metequiv2  15473  metrest  15483  metcnp3  15488  ivthinclemlopn  15613  ivthinclemlr  15614  ivthinclemuopn  15615  ivthinclemur  15616  ivthinclemloc  15618  plycolemc  15735  mpodvdsmulf1o  15970  perfectlem2  15980  2sqlem5  16104  2sqlem6  16105  2sqlem8  16108  2sqlem10  16110  nconstwlpolem  16963