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  2633  rexlimdvaa  2649  issod  4407  ordsuc  4652  fcof1  5900  riota5f  5974  ovmpodf  6127  tfrlemi1  6468  eqsuptid  7152  eqinftid  7176  ordiso2  7190  addnq0mo  7622  mulnq0mo  7623  genprndl  7696  genprndu  7697  addlocpr  7711  ltexprlemm  7775  ltexprlemopl  7776  ltexprlemopu  7778  ltexprlemfl  7784  ltexprlemfu  7786  aptiprleml  7814  caucvgprprlemexbt  7881  addsrmo  7918  mulsrmo  7919  prodge0  8989  un0addcl  9390  un0mulcl  9391  seq3fveq2  10684  seqfveq2g  10686  seq3shft2  10690  seqshft2g  10691  monoord  10694  seq3split  10697  seqsplitg  10698  seqf1oglem1  10728  seq3id2  10735  seqhomog  10739  expnegzap  10782  expcanlem  10924  bcval5  10972  seq3coll  11051  wrdind  11240  wrd2ind  11241  caucvgrelemcau  11477  cau3lem  11611  reccn2ap  11810  summodclem2  11879  zsumdc  11881  fsumf1o  11887  fisumss  11889  fsumcl2lem  11895  fsumadd  11903  fisum0diag2  11944  fsummulc2  11945  mertenslem2  12033  prodmodclem2  12074  zproddc  12076  fprodseq  12080  fprodf1o  12085  prodssdc  12086  fprodssdc  12087  fprodmul  12088  dvds0lem  12298  dvdsnegb  12305  dvdssub2  12332  isprm6  12655  hashgcdeq  12748  modprminv  12758  modprminveq  12759  reumodprminv  12762  pcqmul  12812  pcqcl  12815  pcxnn0cl  12819  pcxcl  12820  pc2dvds  12839  pcadd  12849  pcmpt  12852  pockthg  12866  infpnlem1  12868  mgmidsssn0  13403  mhmeql  13511  grprcan  13556  dfgrp3mlem  13617  mulgnn0ass  13681  isnsg3  13730  ghmpreima  13789  ghmeql  13790  lss1d  14332  znidomb  14607  topssnei  14821  innei  14822  cnptopco  14881  cncnpi  14887  cncnp  14889  cnconst2  14892  cnpdis  14901  lmtopcnp  14909  tx2cn  14929  txdis  14936  blssps  15086  blss  15087  neibl  15150  metss  15153  metequiv2  15155  metrest  15165  metcnp3  15170  ivthinclemlopn  15295  ivthinclemlr  15296  ivthinclemuopn  15297  ivthinclemur  15298  ivthinclemloc  15300  plycolemc  15417  mpodvdsmulf1o  15649  perfectlem2  15659  2sqlem5  15783  2sqlem6  15784  2sqlem8  15787  2sqlem10  15789  nconstwlpolem  16364