Theorem expr 373

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 363	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp 123	1 |- ( ( ph /\ ps ) -> ( ch -> th ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  animpimp2impd  549  reximddv  2560  rexlimdvaa  2575  issod  4278  ordsuc  4520  fcof1  5728  riota5f  5798  ovmpodf  5946  tfrlemi1  6273  eqsuptid  6933  eqinftid  6957  ordiso2  6969  addnq0mo  7350  mulnq0mo  7351  genprndl  7424  genprndu  7425  addlocpr  7439  ltexprlemm  7503  ltexprlemopl  7504  ltexprlemopu  7506  ltexprlemfl  7512  ltexprlemfu  7514  aptiprleml  7542  caucvgprprlemexbt  7609  addsrmo  7646  mulsrmo  7647  prodge0  8708  un0addcl  9106  un0mulcl  9107  seq3fveq2  10350  seq3shft2  10354  monoord  10357  seq3split  10360  seq3id2  10390  expnegzap  10435  expcanlem  10571  bcval5  10619  seq3coll  10695  caucvgrelemcau  10862  cau3lem  10996  reccn2ap  11192  summodclem2  11261  zsumdc  11263  fsumf1o  11269  fisumss  11271  fsumcl2lem  11277  fsumadd  11285  fisum0diag2  11326  fsummulc2  11327  mertenslem2  11415  prodmodclem2  11456  zproddc  11458  fprodseq  11462  fprodf1o  11467  prodssdc  11468  fprodssdc  11469  fprodmul  11470  dvds0lem  11678  dvdsnegb  11685  dvdssub2  11710  isprm6  12001  hashgcdeq  12091  topssnei  12522  innei  12523  cnptopco  12582  cncnpi  12588  cncnp  12590  cnconst2  12593  cnpdis  12602  lmtopcnp  12610  tx2cn  12630  txdis  12637  blssps  12787  blss  12788  neibl  12851  metss  12854  metequiv2  12856  metrest  12866  metcnp3  12871  ivthinclemlopn  12974  ivthinclemlr  12975  ivthinclemuopn  12976  ivthinclemur  12977  ivthinclemloc  12979  nconstwlpolem  13597