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  2645  rexlimdvaa  2661  issod  4439  ordsuc  4684  fcof1  5955  riota5f  6029  ovmpodf  6184  suppssdc  6459  tfrlemi1  6562  eqsuptid  7287  eqinftid  7311  ordiso2  7325  addnq0mo  7761  mulnq0mo  7762  genprndl  7835  genprndu  7836  addlocpr  7850  ltexprlemm  7914  ltexprlemopl  7915  ltexprlemopu  7917  ltexprlemfl  7923  ltexprlemfu  7925  aptiprleml  7953  caucvgprprlemexbt  8020  addsrmo  8057  mulsrmo  8058  prodge0  9127  un0addcl  9528  un0mulcl  9529  seq3fveq2  10836  seqfveq2g  10838  seq3shft2  10842  seqshft2g  10843  monoord  10846  seq3split  10849  seqsplitg  10850  seqf1oglem1  10880  seq3id2  10887  seqhomog  10891  expnegzap  10934  expcanlem  11076  bcval5  11124  hashfibc  11203  seq3coll  11210  wrdind  11410  wrd2ind  11411  caucvgrelemcau  11661  cau3lem  11795  reccn2ap  11994  summodclem2  12064  zsumdc  12066  fsumf1o  12072  fisumss  12074  fsumcl2lem  12080  fsumadd  12088  fisum0diag2  12129  fsummulc2  12130  mertenslem2  12218  prodmodclem2  12259  zproddc  12261  fprodseq  12265  fprodf1o  12270  prodssdc  12271  fprodssdc  12272  fprodmul  12273  dvds0lem  12483  dvdsnegb  12490  dvdssub2  12517  isprm6  12840  hashgcdeq  12933  modprminv  12943  modprminveq  12944  reumodprminv  12947  pcqmul  12997  pcqcl  13000  pcxnn0cl  13004  pcxcl  13005  pc2dvds  13024  pcadd  13034  pcmpt  13037  pockthg  13051  infpnlem1  13053  mgmidsssn0  13589  mhmeql  13697  grprcan  13742  dfgrp3mlem  13803  mulgnn0ass  13867  isnsg3  13916  ghmpreima  13975  ghmeql  13976  lss1d  14523  znidomb  14798  topssnei  15019  innei  15020  cnptopco  15079  cncnpi  15085  cncnp  15087  cnconst2  15090  cnpdis  15099  lmtopcnp  15107  tx2cn  15127  txdis  15134  blssps  15284  blss  15285  neibl  15348  metss  15351  metequiv2  15353  metrest  15363  metcnp3  15368  ivthinclemlopn  15493  ivthinclemlr  15494  ivthinclemuopn  15495  ivthinclemur  15496  ivthinclemloc  15498  plycolemc  15615  mpodvdsmulf1o  15850  perfectlem2  15860  2sqlem5  15984  2sqlem6  15985  2sqlem8  15988  2sqlem10  15990  nconstwlpolem  16842