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  4354  ordsuc  4599  fcof1  5830  riota5f  5902  ovmpodf  6054  tfrlemi1  6390  eqsuptid  7063  eqinftid  7087  ordiso2  7101  addnq0mo  7514  mulnq0mo  7515  genprndl  7588  genprndu  7589  addlocpr  7603  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemfl  7676  ltexprlemfu  7678  aptiprleml  7706  caucvgprprlemexbt  7773  addsrmo  7810  mulsrmo  7811  prodge0  8881  un0addcl  9282  un0mulcl  9283  seq3fveq2  10567  seqfveq2g  10569  seq3shft2  10573  seqshft2g  10574  monoord  10577  seq3split  10580  seqsplitg  10581  seqf1oglem1  10611  seq3id2  10618  seqhomog  10622  expnegzap  10665  expcanlem  10807  bcval5  10855  seq3coll  10934  caucvgrelemcau  11145  cau3lem  11279  reccn2ap  11478  summodclem2  11547  zsumdc  11549  fsumf1o  11555  fisumss  11557  fsumcl2lem  11563  fsumadd  11571  fisum0diag2  11612  fsummulc2  11613  mertenslem2  11701  prodmodclem2  11742  zproddc  11744  fprodseq  11748  fprodf1o  11753  prodssdc  11754  fprodssdc  11755  fprodmul  11756  dvds0lem  11966  dvdsnegb  11973  dvdssub2  12000  isprm6  12315  hashgcdeq  12408  modprminv  12418  modprminveq  12419  reumodprminv  12422  pcqmul  12472  pcqcl  12475  pcxnn0cl  12479  pcxcl  12480  pc2dvds  12499  pcadd  12509  pcmpt  12512  pockthg  12526  infpnlem1  12528  mgmidsssn0  13027  mhmeql  13124  grprcan  13169  dfgrp3mlem  13230  mulgnn0ass  13288  isnsg3  13337  ghmpreima  13396  ghmeql  13397  lss1d  13939  znidomb  14214  topssnei  14398  innei  14399  cnptopco  14458  cncnpi  14464  cncnp  14466  cnconst2  14469  cnpdis  14478  lmtopcnp  14486  tx2cn  14506  txdis  14513  blssps  14663  blss  14664  neibl  14727  metss  14730  metequiv2  14732  metrest  14742  metcnp3  14747  ivthinclemlopn  14872  ivthinclemlr  14873  ivthinclemuopn  14874  ivthinclemur  14875  ivthinclemloc  14877  plycolemc  14994  mpodvdsmulf1o  15226  perfectlem2  15236  2sqlem5  15360  2sqlem6  15361  2sqlem8  15364  2sqlem10  15366  nconstwlpolem  15709