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  2635  rexlimdvaa  2651  issod  4416  ordsuc  4661  fcof1  5924  riota5f  5998  ovmpodf  6153  tfrlemi1  6498  eqsuptid  7196  eqinftid  7220  ordiso2  7234  addnq0mo  7667  mulnq0mo  7668  genprndl  7741  genprndu  7742  addlocpr  7756  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemfl  7829  ltexprlemfu  7831  aptiprleml  7859  caucvgprprlemexbt  7926  addsrmo  7963  mulsrmo  7964  prodge0  9034  un0addcl  9435  un0mulcl  9436  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  seqf1oglem1  10782  seq3id2  10789  seqhomog  10793  expnegzap  10836  expcanlem  10978  bcval5  11026  seq3coll  11107  wrdind  11307  wrd2ind  11308  caucvgrelemcau  11545  cau3lem  11679  reccn2ap  11878  summodclem2  11948  zsumdc  11950  fsumf1o  11956  fisumss  11958  fsumcl2lem  11964  fsumadd  11972  fisum0diag2  12013  fsummulc2  12014  mertenslem2  12102  prodmodclem2  12143  zproddc  12145  fprodseq  12149  fprodf1o  12154  prodssdc  12155  fprodssdc  12156  fprodmul  12157  dvds0lem  12367  dvdsnegb  12374  dvdssub2  12401  isprm6  12724  hashgcdeq  12817  modprminv  12827  modprminveq  12828  reumodprminv  12831  pcqmul  12881  pcqcl  12884  pcxnn0cl  12888  pcxcl  12889  pc2dvds  12908  pcadd  12918  pcmpt  12921  pockthg  12935  infpnlem1  12937  mgmidsssn0  13472  mhmeql  13580  grprcan  13625  dfgrp3mlem  13686  mulgnn0ass  13750  isnsg3  13799  ghmpreima  13858  ghmeql  13859  lss1d  14403  znidomb  14678  topssnei  14892  innei  14893  cnptopco  14952  cncnpi  14958  cncnp  14960  cnconst2  14963  cnpdis  14972  lmtopcnp  14980  tx2cn  15000  txdis  15007  blssps  15157  blss  15158  neibl  15221  metss  15224  metequiv2  15226  metrest  15236  metcnp3  15241  ivthinclemlopn  15366  ivthinclemlr  15367  ivthinclemuopn  15368  ivthinclemur  15369  ivthinclemloc  15371  plycolemc  15488  mpodvdsmulf1o  15720  perfectlem2  15730  2sqlem5  15854  2sqlem6  15855  2sqlem8  15858  2sqlem10  15860  nconstwlpolem  16695