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  2600  rexlimdvaa  2615  issod  4355  ordsuc  4600  fcof1  5833  riota5f  5905  ovmpodf  6058  tfrlemi1  6399  eqsuptid  7072  eqinftid  7096  ordiso2  7110  addnq0mo  7533  mulnq0mo  7534  genprndl  7607  genprndu  7608  addlocpr  7622  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemfl  7695  ltexprlemfu  7697  aptiprleml  7725  caucvgprprlemexbt  7792  addsrmo  7829  mulsrmo  7830  prodge0  8900  un0addcl  9301  un0mulcl  9302  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord  10596  seq3split  10599  seqsplitg  10600  seqf1oglem1  10630  seq3id2  10637  seqhomog  10641  expnegzap  10684  expcanlem  10826  bcval5  10874  seq3coll  10953  caucvgrelemcau  11164  cau3lem  11298  reccn2ap  11497  summodclem2  11566  zsumdc  11568  fsumf1o  11574  fisumss  11576  fsumcl2lem  11582  fsumadd  11590  fisum0diag2  11631  fsummulc2  11632  mertenslem2  11720  prodmodclem2  11761  zproddc  11763  fprodseq  11767  fprodf1o  11772  prodssdc  11773  fprodssdc  11774  fprodmul  11775  dvds0lem  11985  dvdsnegb  11992  dvdssub2  12019  isprm6  12342  hashgcdeq  12435  modprminv  12445  modprminveq  12446  reumodprminv  12449  pcqmul  12499  pcqcl  12502  pcxnn0cl  12506  pcxcl  12507  pc2dvds  12526  pcadd  12536  pcmpt  12539  pockthg  12553  infpnlem1  12555  mgmidsssn0  13088  mhmeql  13196  grprcan  13241  dfgrp3mlem  13302  mulgnn0ass  13366  isnsg3  13415  ghmpreima  13474  ghmeql  13475  lss1d  14017  znidomb  14292  topssnei  14506  innei  14507  cnptopco  14566  cncnpi  14572  cncnp  14574  cnconst2  14577  cnpdis  14586  lmtopcnp  14594  tx2cn  14614  txdis  14621  blssps  14771  blss  14772  neibl  14835  metss  14838  metequiv2  14840  metrest  14850  metcnp3  14855  ivthinclemlopn  14980  ivthinclemlr  14981  ivthinclemuopn  14982  ivthinclemur  14983  ivthinclemloc  14985  plycolemc  15102  mpodvdsmulf1o  15334  perfectlem2  15344  2sqlem5  15468  2sqlem6  15469  2sqlem8  15472  2sqlem10  15474  nconstwlpolem  15822