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  4414  ordsuc  4659  fcof1  5919  riota5f  5993  ovmpodf  6148  tfrlemi1  6493  eqsuptid  7190  eqinftid  7214  ordiso2  7228  addnq0mo  7660  mulnq0mo  7661  genprndl  7734  genprndu  7735  addlocpr  7749  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemopu  7816  ltexprlemfl  7822  ltexprlemfu  7824  aptiprleml  7852  caucvgprprlemexbt  7919  addsrmo  7956  mulsrmo  7957  prodge0  9027  un0addcl  9428  un0mulcl  9429  seq3fveq2  10730  seqfveq2g  10732  seq3shft2  10736  seqshft2g  10737  monoord  10740  seq3split  10743  seqsplitg  10744  seqf1oglem1  10774  seq3id2  10781  seqhomog  10785  expnegzap  10828  expcanlem  10970  bcval5  11018  seq3coll  11099  wrdind  11296  wrd2ind  11297  caucvgrelemcau  11534  cau3lem  11668  reccn2ap  11867  summodclem2  11936  zsumdc  11938  fsumf1o  11944  fisumss  11946  fsumcl2lem  11952  fsumadd  11960  fisum0diag2  12001  fsummulc2  12002  mertenslem2  12090  prodmodclem2  12131  zproddc  12133  fprodseq  12137  fprodf1o  12142  prodssdc  12143  fprodssdc  12144  fprodmul  12145  dvds0lem  12355  dvdsnegb  12362  dvdssub2  12389  isprm6  12712  hashgcdeq  12805  modprminv  12815  modprminveq  12816  reumodprminv  12819  pcqmul  12869  pcqcl  12872  pcxnn0cl  12876  pcxcl  12877  pc2dvds  12896  pcadd  12906  pcmpt  12909  pockthg  12923  infpnlem1  12925  mgmidsssn0  13460  mhmeql  13568  grprcan  13613  dfgrp3mlem  13674  mulgnn0ass  13738  isnsg3  13787  ghmpreima  13846  ghmeql  13847  lss1d  14390  znidomb  14665  topssnei  14879  innei  14880  cnptopco  14939  cncnpi  14945  cncnp  14947  cnconst2  14950  cnpdis  14959  lmtopcnp  14967  tx2cn  14987  txdis  14994  blssps  15144  blss  15145  neibl  15208  metss  15211  metequiv2  15213  metrest  15223  metcnp3  15228  ivthinclemlopn  15353  ivthinclemlr  15354  ivthinclemuopn  15355  ivthinclemur  15356  ivthinclemloc  15358  plycolemc  15475  mpodvdsmulf1o  15707  perfectlem2  15717  2sqlem5  15841  2sqlem6  15842  2sqlem8  15845  2sqlem10  15847  nconstwlpolem  16619