Theorem expl 648

Description: Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)

Hypothesis

Ref	Expression
expl.1	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Assertion

Ref	Expression
expl	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Proof of Theorem expl

Step	Hyp	Ref	Expression
1		expl.1	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
2	1	exp31 630	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	impd 447	1 |- ( ph -> ( ( ps /\ ch ) -> th ) )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  reximd2a  3013  tfindsg2  7061  tz7.49c  7541  ssenen  8134  pssnn  8178  unwdomg  8489  cff1  9080  cfsmolem  9092  cfpwsdom  9406  wunex2  9560  mulgt0sr  9926  uzwo  11751  shftfval  13810  fsum2dlem  14501  fprod2dlem  14710  prmpwdvds  15608  quscrng  19240  chfacfscmul0  20663  chfacfpmmul0  20667  tgtop  20777  neitr  20984  bwth  21213  tx1stc  21453  cnextcn  21871  logfac2  24942  axcontlem12  25855  spanuni  28403  pjnmopi  29007  superpos  29213  atcvat4i  29256  rabeqsnd  29342  fpwrelmap  29508  2sqmo  29649  locfinreflem  29907  cmpcref  29917  fneint  32343  neibastop3  32357  bj-ismooredr2  33065  isbasisrelowllem1  33203  isbasisrelowllem2  33204  relowlssretop  33211  finxpreclem6  33233  fin2so  33396  matunitlindflem2  33406  poimirlem26  33435  poimirlem27  33436  heicant  33444  ismblfin  33450  ovoliunnfl  33451  itg2gt0cn  33465  cvrat4  34729  pell14qrexpcl  37431  odz2prm2pw  41475