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  2597  rexlimdvaa  2612  issod  4351  ordsuc  4596  fcof1  5827  riota5f  5899  ovmpodf  6051  tfrlemi1  6387  eqsuptid  7058  eqinftid  7082  ordiso2  7096  addnq0mo  7509  mulnq0mo  7510  genprndl  7583  genprndu  7584  addlocpr  7598  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemfl  7671  ltexprlemfu  7673  aptiprleml  7701  caucvgprprlemexbt  7768  addsrmo  7805  mulsrmo  7806  prodge0  8875  un0addcl  9276  un0mulcl  9277  seq3fveq2  10549  seqfveq2g  10551  seq3shft2  10555  seqshft2g  10556  monoord  10559  seq3split  10562  seqsplitg  10563  seqf1oglem1  10593  seq3id2  10600  seqhomog  10604  expnegzap  10647  expcanlem  10789  bcval5  10837  seq3coll  10916  caucvgrelemcau  11127  cau3lem  11261  reccn2ap  11459  summodclem2  11528  zsumdc  11530  fsumf1o  11536  fisumss  11538  fsumcl2lem  11544  fsumadd  11552  fisum0diag2  11593  fsummulc2  11594  mertenslem2  11682  prodmodclem2  11723  zproddc  11725  fprodseq  11729  fprodf1o  11734  prodssdc  11735  fprodssdc  11736  fprodmul  11737  dvds0lem  11947  dvdsnegb  11954  dvdssub2  11981  isprm6  12288  hashgcdeq  12380  modprminv  12390  modprminveq  12391  reumodprminv  12394  pcqmul  12444  pcqcl  12447  pcxnn0cl  12451  pcxcl  12452  pc2dvds  12471  pcadd  12481  pcmpt  12484  pockthg  12498  infpnlem1  12500  mgmidsssn0  12970  mhmeql  13067  grprcan  13112  dfgrp3mlem  13173  mulgnn0ass  13231  isnsg3  13280  ghmpreima  13339  ghmeql  13340  lss1d  13882  znidomb  14157  topssnei  14341  innei  14342  cnptopco  14401  cncnpi  14407  cncnp  14409  cnconst2  14412  cnpdis  14421  lmtopcnp  14429  tx2cn  14449  txdis  14456  blssps  14606  blss  14607  neibl  14670  metss  14673  metequiv2  14675  metrest  14685  metcnp3  14690  ivthinclemlopn  14815  ivthinclemlr  14816  ivthinclemuopn  14817  ivthinclemur  14818  ivthinclemloc  14820  plycolemc  14936  2sqlem5  15276  2sqlem6  15277  2sqlem8  15280  2sqlem10  15282  nconstwlpolem  15625