MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expl Structured version   Visualization version   GIF version

Theorem expl 458
Description: Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
Hypothesis
Ref Expression
expl.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
expl (𝜑 → ((𝜓𝜒) → 𝜃))

Proof of Theorem expl
StepHypRef Expression
1 expl.1 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
21exp31 420 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 411 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  reximd2a  3309  tfindsg2  7565  tz7.49c  8071  ssenen  8679  pssnn  8724  unwdomg  9036  cff1  9668  cfsmolem  9680  cfpwsdom  9994  wunex2  10148  mulgt0sr  10515  uzwo  12299  shftfval  14417  fsum2dlem  15113  fprod2dlem  15322  prmpwdvds  16228  quscrng  19941  chfacfscmul0  21394  chfacfpmmul0  21398  tgtop  21509  neitr  21716  bwth  21946  tx1stc  22186  cnextcn  22603  logfac2  25720  2sqmo  25940  outpasch  26468  trgcopyeu  26519  axcontlem12  26688  spanuni  29248  pjnmopi  29852  superpos  30058  atcvat4i  30101  rabeqsnd  30191  fpwrelmap  30395  locfinreflem  31003  cmpcref  31013  loop1cycl  32281  fneint  33593  neibastop3  33607  isbasisrelowllem1  34518  isbasisrelowllem2  34519  relowlssretop  34526  finxpreclem6  34559  ralssiun  34570  fin2so  34760  matunitlindflem2  34770  poimirlem26  34799  poimirlem27  34800  heicant  34808  ismblfin  34814  ovoliunnfl  34815  itg2gt0cn  34828  cvrat4  36459  pell14qrexpcl  39342  liminflimsupxrre  41974  odz2prm2pw  43602  prelrrx2b  44629
  Copyright terms: Public domain W3C validator