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  2610  rexlimdvaa  2625  issod  4370  ordsuc  4615  fcof1  5859  riota5f  5931  ovmpodf  6084  tfrlemi1  6425  eqsuptid  7106  eqinftid  7130  ordiso2  7144  addnq0mo  7567  mulnq0mo  7568  genprndl  7641  genprndu  7642  addlocpr  7656  ltexprlemm  7720  ltexprlemopl  7721  ltexprlemopu  7723  ltexprlemfl  7729  ltexprlemfu  7731  aptiprleml  7759  caucvgprprlemexbt  7826  addsrmo  7863  mulsrmo  7864  prodge0  8934  un0addcl  9335  un0mulcl  9336  seq3fveq2  10627  seqfveq2g  10629  seq3shft2  10633  seqshft2g  10634  monoord  10637  seq3split  10640  seqsplitg  10641  seqf1oglem1  10671  seq3id2  10678  seqhomog  10682  expnegzap  10725  expcanlem  10867  bcval5  10915  seq3coll  10994  caucvgrelemcau  11335  cau3lem  11469  reccn2ap  11668  summodclem2  11737  zsumdc  11739  fsumf1o  11745  fisumss  11747  fsumcl2lem  11753  fsumadd  11761  fisum0diag2  11802  fsummulc2  11803  mertenslem2  11891  prodmodclem2  11932  zproddc  11934  fprodseq  11938  fprodf1o  11943  prodssdc  11944  fprodssdc  11945  fprodmul  11946  dvds0lem  12156  dvdsnegb  12163  dvdssub2  12190  isprm6  12513  hashgcdeq  12606  modprminv  12616  modprminveq  12617  reumodprminv  12620  pcqmul  12670  pcqcl  12673  pcxnn0cl  12677  pcxcl  12678  pc2dvds  12697  pcadd  12707  pcmpt  12710  pockthg  12724  infpnlem1  12726  mgmidsssn0  13260  mhmeql  13368  grprcan  13413  dfgrp3mlem  13474  mulgnn0ass  13538  isnsg3  13587  ghmpreima  13646  ghmeql  13647  lss1d  14189  znidomb  14464  topssnei  14678  innei  14679  cnptopco  14738  cncnpi  14744  cncnp  14746  cnconst2  14749  cnpdis  14758  lmtopcnp  14766  tx2cn  14786  txdis  14793  blssps  14943  blss  14944  neibl  15007  metss  15010  metequiv2  15012  metrest  15022  metcnp3  15027  ivthinclemlopn  15152  ivthinclemlr  15153  ivthinclemuopn  15154  ivthinclemur  15155  ivthinclemloc  15157  plycolemc  15274  mpodvdsmulf1o  15506  perfectlem2  15516  2sqlem5  15640  2sqlem6  15641  2sqlem8  15644  2sqlem10  15646  nconstwlpolem  16078