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  2580  rexlimdvaa  2595  issod  4320  ordsuc  4563  fcof1  5784  riota5f  5855  ovmpodf  6006  tfrlemi1  6333  eqsuptid  6996  eqinftid  7020  ordiso2  7034  addnq0mo  7446  mulnq0mo  7447  genprndl  7520  genprndu  7521  addlocpr  7535  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemfl  7608  ltexprlemfu  7610  aptiprleml  7638  caucvgprprlemexbt  7705  addsrmo  7742  mulsrmo  7743  prodge0  8811  un0addcl  9209  un0mulcl  9210  seq3fveq2  10469  seq3shft2  10473  monoord  10476  seq3split  10479  seq3id2  10509  expnegzap  10554  expcanlem  10695  bcval5  10743  seq3coll  10822  caucvgrelemcau  10989  cau3lem  11123  reccn2ap  11321  summodclem2  11390  zsumdc  11392  fsumf1o  11398  fisumss  11400  fsumcl2lem  11406  fsumadd  11414  fisum0diag2  11455  fsummulc2  11456  mertenslem2  11544  prodmodclem2  11585  zproddc  11587  fprodseq  11591  fprodf1o  11596  prodssdc  11597  fprodssdc  11598  fprodmul  11599  dvds0lem  11808  dvdsnegb  11815  dvdssub2  11842  isprm6  12147  hashgcdeq  12239  modprminv  12249  modprminveq  12250  reumodprminv  12253  pcqmul  12303  pcqcl  12306  pcxnn0cl  12310  pcxcl  12311  pc2dvds  12329  pcadd  12339  pcmpt  12341  pockthg  12355  infpnlem1  12357  mgmidsssn0  12803  mhmeql  12876  grprcan  12910  dfgrp3mlem  12968  mulgnn0ass  13019  isnsg3  13067  topssnei  13665  innei  13666  cnptopco  13725  cncnpi  13731  cncnp  13733  cnconst2  13736  cnpdis  13745  lmtopcnp  13753  tx2cn  13773  txdis  13780  blssps  13930  blss  13931  neibl  13994  metss  13997  metequiv2  13999  metrest  14009  metcnp3  14014  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemloc  14122  2sqlem5  14469  2sqlem6  14470  2sqlem8  14473  2sqlem10  14475  nconstwlpolem  14815