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  2600  rexlimdvaa  2615  issod  4355  ordsuc  4600  fcof1  5833  riota5f  5905  ovmpodf  6058  tfrlemi1  6399  eqsuptid  7072  eqinftid  7096  ordiso2  7110  addnq0mo  7531  mulnq0mo  7532  genprndl  7605  genprndu  7606  addlocpr  7620  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemfl  7693  ltexprlemfu  7695  aptiprleml  7723  caucvgprprlemexbt  7790  addsrmo  7827  mulsrmo  7828  prodge0  8898  un0addcl  9299  un0mulcl  9300  seq3fveq2  10584  seqfveq2g  10586  seq3shft2  10590  seqshft2g  10591  monoord  10594  seq3split  10597  seqsplitg  10598  seqf1oglem1  10628  seq3id2  10635  seqhomog  10639  expnegzap  10682  expcanlem  10824  bcval5  10872  seq3coll  10951  caucvgrelemcau  11162  cau3lem  11296  reccn2ap  11495  summodclem2  11564  zsumdc  11566  fsumf1o  11572  fisumss  11574  fsumcl2lem  11580  fsumadd  11588  fisum0diag2  11629  fsummulc2  11630  mertenslem2  11718  prodmodclem2  11759  zproddc  11761  fprodseq  11765  fprodf1o  11770  prodssdc  11771  fprodssdc  11772  fprodmul  11773  dvds0lem  11983  dvdsnegb  11990  dvdssub2  12017  isprm6  12340  hashgcdeq  12433  modprminv  12443  modprminveq  12444  reumodprminv  12447  pcqmul  12497  pcqcl  12500  pcxnn0cl  12504  pcxcl  12505  pc2dvds  12524  pcadd  12534  pcmpt  12537  pockthg  12551  infpnlem1  12553  mgmidsssn0  13086  mhmeql  13194  grprcan  13239  dfgrp3mlem  13300  mulgnn0ass  13364  isnsg3  13413  ghmpreima  13472  ghmeql  13473  lss1d  14015  znidomb  14290  topssnei  14482  innei  14483  cnptopco  14542  cncnpi  14548  cncnp  14550  cnconst2  14553  cnpdis  14562  lmtopcnp  14570  tx2cn  14590  txdis  14597  blssps  14747  blss  14748  neibl  14811  metss  14814  metequiv2  14816  metrest  14826  metcnp3  14831  ivthinclemlopn  14956  ivthinclemlr  14957  ivthinclemuopn  14958  ivthinclemur  14959  ivthinclemloc  14961  plycolemc  15078  mpodvdsmulf1o  15310  perfectlem2  15320  2sqlem5  15444  2sqlem6  15445  2sqlem8  15448  2sqlem10  15450  nconstwlpolem  15796