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  4466  ordsuc  4712  fcof1  5992  riota5f  6068  ovmpodf  6223  suppssdc  6504  tfrlemi1  6607  eqsuptid  7344  eqinftid  7368  ordiso2  7382  addnq0mo  7821  mulnq0mo  7822  genprndl  7895  genprndu  7896  addlocpr  7910  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemfl  7983  ltexprlemfu  7985  aptiprleml  8013  caucvgprprlemexbt  8080  addsrmo  8117  mulsrmo  8118  prodge0  9193  un0addcl  9608  un0mulcl  9609  seq3fveq2  10934  seqfveq2g  10936  seq3shft2  10940  seqshft2g  10941  monoord  10944  seq3split  10947  seqsplitg  10948  seqf1oglem1  10978  seq3id2  10985  seqhomog  10989  expnegzap  11032  expcanlem  11176  bcval5  11224  hashfibc  11306  seq3coll  11317  wrdind  11517  wrd2ind  11518  caucvgrelemcau  11769  cau3lem  11904  reccn2ap  12105  summodclem2  12175  zsumdc  12177  fsumf1o  12183  fisumss  12185  fsumcl2lem  12191  fsumadd  12199  fisum0diag2  12240  fsummulc2  12241  mertenslem2  12329  prodmodclem2  12370  zproddc  12372  fprodseq  12376  fprodf1o  12381  prodssdc  12382  fprodssdc  12383  fprodmul  12384  dvds0lem  12594  dvdsnegb  12601  dvdssub2  12628  isprm6  12952  hashgcdeq  13048  modprminv  13058  modprminveq  13059  reumodprminv  13062  pcqmul  13112  pcqcl  13115  pcxnn0cl  13119  pcxcl  13120  pc2dvds  13139  pcadd  13149  pcmpt  13152  pockthg  13166  infpnlem1  13168  ballotfilemfc0  13291  ballotfilemfcc  13292  mgmidsssn0  13764  mhmeql  13859  grprcan  13902  dfgrp3mlem  13963  mulgnn0ass  14021  isnsg3  14070  ghmpreima  14129  ghmeql  14130  lss1d  14830  znidomb  15103  rnasclassa  15148  mvrf1fi  15215  topssnei  15400  innei  15401  cnptopco  15460  cncnpi  15466  cncnp  15468  cnconst2  15471  cnpdis  15480  lmtopcnp  15488  tx2cn  15508  txdis  15515  blssps  15665  blss  15666  neibl  15729  metss  15732  metequiv2  15734  metrest  15744  metcnp3  15749  ivthinclemlopn  15874  ivthinclemlr  15875  ivthinclemuopn  15876  ivthinclemur  15877  ivthinclemloc  15879  plycolemc  15996  rpcxpmul2z  16160  ppinprm  16272  chtnprm  16274  mpodvdsmulf1o  16296  chtublem  16307  perfectlem2  16312  bposlem1  16323  bposlem3  16325  2sqlem5  16455  2sqlem6  16456  2sqlem8  16459  2sqlem10  16461  nconstwlpolem  17334