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  2593  rexlimdvaa  2608  issod  4334  ordsuc  4577  fcof1  5801  riota5f  5872  ovmpodf  6024  tfrlemi1  6352  eqsuptid  7016  eqinftid  7040  ordiso2  7054  addnq0mo  7466  mulnq0mo  7467  genprndl  7540  genprndu  7541  addlocpr  7555  ltexprlemm  7619  ltexprlemopl  7620  ltexprlemopu  7622  ltexprlemfl  7628  ltexprlemfu  7630  aptiprleml  7658  caucvgprprlemexbt  7725  addsrmo  7762  mulsrmo  7763  prodge0  8831  un0addcl  9229  un0mulcl  9230  seq3fveq2  10489  seq3shft2  10493  monoord  10496  seq3split  10499  seq3id2  10529  expnegzap  10574  expcanlem  10715  bcval5  10763  seq3coll  10842  caucvgrelemcau  11009  cau3lem  11143  reccn2ap  11341  summodclem2  11410  zsumdc  11412  fsumf1o  11418  fisumss  11420  fsumcl2lem  11426  fsumadd  11434  fisum0diag2  11475  fsummulc2  11476  mertenslem2  11564  prodmodclem2  11605  zproddc  11607  fprodseq  11611  fprodf1o  11616  prodssdc  11617  fprodssdc  11618  fprodmul  11619  dvds0lem  11828  dvdsnegb  11835  dvdssub2  11862  isprm6  12167  hashgcdeq  12259  modprminv  12269  modprminveq  12270  reumodprminv  12273  pcqmul  12323  pcqcl  12326  pcxnn0cl  12330  pcxcl  12331  pc2dvds  12349  pcadd  12359  pcmpt  12361  pockthg  12375  infpnlem1  12377  mgmidsssn0  12833  mhmeql  12917  grprcan  12954  dfgrp3mlem  13015  mulgnn0ass  13071  isnsg3  13119  ghmpreima  13173  ghmeql  13174  lss1d  13667  topssnei  14066  innei  14067  cnptopco  14126  cncnpi  14132  cncnp  14134  cnconst2  14137  cnpdis  14146  lmtopcnp  14154  tx2cn  14174  txdis  14181  blssps  14331  blss  14332  neibl  14395  metss  14398  metequiv2  14400  metrest  14410  metcnp3  14415  ivthinclemlopn  14518  ivthinclemlr  14519  ivthinclemuopn  14520  ivthinclemur  14521  ivthinclemloc  14523  2sqlem5  14870  2sqlem6  14871  2sqlem8  14874  2sqlem10  14876  nconstwlpolem  15218