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  561  reximddv  2647  rexlimdvaa  2663  issod  4445  ordsuc  4690  fcof1  5962  riota5f  6038  ovmpodf  6193  suppssdc  6473  tfrlemi1  6576  eqsuptid  7301  eqinftid  7325  ordiso2  7339  addnq0mo  7778  mulnq0mo  7779  genprndl  7852  genprndu  7853  addlocpr  7867  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemfl  7940  ltexprlemfu  7942  aptiprleml  7970  caucvgprprlemexbt  8037  addsrmo  8074  mulsrmo  8075  prodge0  9148  un0addcl  9549  un0mulcl  9550  seq3fveq2  10864  seqfveq2g  10866  seq3shft2  10870  seqshft2g  10871  monoord  10874  seq3split  10877  seqsplitg  10878  seqf1oglem1  10908  seq3id2  10915  seqhomog  10919  expnegzap  10962  expcanlem  11105  bcval5  11153  hashfibc  11235  seq3coll  11242  wrdind  11442  wrd2ind  11443  caucvgrelemcau  11694  cau3lem  11828  reccn2ap  12027  summodclem2  12097  zsumdc  12099  fsumf1o  12105  fisumss  12107  fsumcl2lem  12113  fsumadd  12121  fisum0diag2  12162  fsummulc2  12163  mertenslem2  12251  prodmodclem2  12292  zproddc  12294  fprodseq  12298  fprodf1o  12303  prodssdc  12304  fprodssdc  12305  fprodmul  12306  dvds0lem  12516  dvdsnegb  12523  dvdssub2  12550  isprm6  12873  hashgcdeq  12966  modprminv  12976  modprminveq  12977  reumodprminv  12980  pcqmul  13030  pcqcl  13033  pcxnn0cl  13037  pcxcl  13038  pc2dvds  13057  pcadd  13067  pcmpt  13070  pockthg  13084  infpnlem1  13086  ballotfilemfc0  13180  ballotfilemfcc  13181  mgmidsssn0  13651  mhmeql  13751  grprcan  13796  dfgrp3mlem  13857  mulgnn0ass  13915  isnsg3  13964  ghmpreima  14023  ghmeql  14024  lss1d  14661  znidomb  14936  topssnei  15157  innei  15158  cnptopco  15217  cncnpi  15223  cncnp  15225  cnconst2  15228  cnpdis  15237  lmtopcnp  15245  tx2cn  15265  txdis  15272  blssps  15422  blss  15423  neibl  15486  metss  15489  metequiv2  15491  metrest  15501  metcnp3  15506  ivthinclemlopn  15631  ivthinclemlr  15632  ivthinclemuopn  15633  ivthinclemur  15634  ivthinclemloc  15636  plycolemc  15753  mpodvdsmulf1o  15988  perfectlem2  15998  2sqlem5  16122  2sqlem6  16123  2sqlem8  16126  2sqlem10  16128  nconstwlpolem  16990