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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  animpimp2impd  565  reximddv  2653  rexlimdvaa  2669  issod  4464  ordsuc  4710  fcof1  5989  riota5f  6065  ovmpodf  6220  suppssdc  6500  tfrlemi1  6603  eqsuptid  7338  eqinftid  7362  ordiso2  7376  addnq0mo  7815  mulnq0mo  7816  genprndl  7889  genprndu  7890  addlocpr  7904  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemfl  7977  ltexprlemfu  7979  aptiprleml  8007  caucvgprprlemexbt  8074  addsrmo  8111  mulsrmo  8112  prodge0  9187  un0addcl  9601  un0mulcl  9602  seq3fveq2  10926  seqfveq2g  10928  seq3shft2  10932  seqshft2g  10933  monoord  10936  seq3split  10939  seqsplitg  10940  seqf1oglem1  10970  seq3id2  10977  seqhomog  10981  expnegzap  11024  expcanlem  11168  bcval5  11216  hashfibc  11298  seq3coll  11309  wrdind  11509  wrd2ind  11510  caucvgrelemcau  11761  cau3lem  11896  reccn2ap  12097  summodclem2  12167  zsumdc  12169  fsumf1o  12175  fisumss  12177  fsumcl2lem  12183  fsumadd  12191  fisum0diag2  12232  fsummulc2  12233  mertenslem2  12321  prodmodclem2  12362  zproddc  12364  fprodseq  12368  fprodf1o  12373  prodssdc  12374  fprodssdc  12375  fprodmul  12376  dvds0lem  12586  dvdsnegb  12593  dvdssub2  12620  isprm6  12944  hashgcdeq  13040  modprminv  13050  modprminveq  13051  reumodprminv  13054  pcqmul  13104  pcqcl  13107  pcxnn0cl  13111  pcxcl  13112  pc2dvds  13131  pcadd  13141  pcmpt  13144  pockthg  13158  infpnlem1  13160  ballotfilemfc0  13283  ballotfilemfcc  13284  mgmidsssn0  13755  mhmeql  13850  grprcan  13893  dfgrp3mlem  13954  mulgnn0ass  14012  isnsg3  14061  ghmpreima  14120  ghmeql  14121  lss1d  14771  znidomb  15044  rnasclassa  15089  topssnei  15315  innei  15316  cnptopco  15375  cncnpi  15381  cncnp  15383  cnconst2  15386  cnpdis  15395  lmtopcnp  15403  tx2cn  15423  txdis  15430  blssps  15580  blss  15581  neibl  15644  metss  15647  metequiv2  15649  metrest  15659  metcnp3  15664  ivthinclemlopn  15789  ivthinclemlr  15790  ivthinclemuopn  15791  ivthinclemur  15792  ivthinclemloc  15794  plycolemc  15911  ppinprm  16182  chtnprm  16184  mpodvdsmulf1o  16206  chtublem  16217  perfectlem2  16222  bposlem1  16233  bposlem3  16235  2sqlem5  16360  2sqlem6  16361  2sqlem8  16364  2sqlem10  16366  nconstwlpolem  17237