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  4411  ordsuc  4656  fcof1  5916  riota5f  5990  ovmpodf  6145  tfrlemi1  6489  eqsuptid  7180  eqinftid  7204  ordiso2  7218  addnq0mo  7650  mulnq0mo  7651  genprndl  7724  genprndu  7725  addlocpr  7739  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemopu  7806  ltexprlemfl  7812  ltexprlemfu  7814  aptiprleml  7842  caucvgprprlemexbt  7909  addsrmo  7946  mulsrmo  7947  prodge0  9017  un0addcl  9418  un0mulcl  9419  seq3fveq2  10714  seqfveq2g  10716  seq3shft2  10720  seqshft2g  10721  monoord  10724  seq3split  10727  seqsplitg  10728  seqf1oglem1  10758  seq3id2  10765  seqhomog  10769  expnegzap  10812  expcanlem  10954  bcval5  11002  seq3coll  11082  wrdind  11275  wrd2ind  11276  caucvgrelemcau  11512  cau3lem  11646  reccn2ap  11845  summodclem2  11914  zsumdc  11916  fsumf1o  11922  fisumss  11924  fsumcl2lem  11930  fsumadd  11938  fisum0diag2  11979  fsummulc2  11980  mertenslem2  12068  prodmodclem2  12109  zproddc  12111  fprodseq  12115  fprodf1o  12120  prodssdc  12121  fprodssdc  12122  fprodmul  12123  dvds0lem  12333  dvdsnegb  12340  dvdssub2  12367  isprm6  12690  hashgcdeq  12783  modprminv  12793  modprminveq  12794  reumodprminv  12797  pcqmul  12847  pcqcl  12850  pcxnn0cl  12854  pcxcl  12855  pc2dvds  12874  pcadd  12884  pcmpt  12887  pockthg  12901  infpnlem1  12903  mgmidsssn0  13438  mhmeql  13546  grprcan  13591  dfgrp3mlem  13652  mulgnn0ass  13716  isnsg3  13765  ghmpreima  13824  ghmeql  13825  lss1d  14368  znidomb  14643  topssnei  14857  innei  14858  cnptopco  14917  cncnpi  14923  cncnp  14925  cnconst2  14928  cnpdis  14937  lmtopcnp  14945  tx2cn  14965  txdis  14972  blssps  15122  blss  15123  neibl  15186  metss  15189  metequiv2  15191  metrest  15201  metcnp3  15206  ivthinclemlopn  15331  ivthinclemlr  15332  ivthinclemuopn  15333  ivthinclemur  15334  ivthinclemloc  15336  plycolemc  15453  mpodvdsmulf1o  15685  perfectlem2  15695  2sqlem5  15819  2sqlem6  15820  2sqlem8  15823  2sqlem10  15825  nconstwlpolem  16547