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  3316  tfindsg2  7567  tz7.49c  8076  ssenen  8683  pssnn  8728  unwdomg  9040  cff1  9672  cfsmolem  9684  cfpwsdom  9998  wunex2  10152  mulgt0sr  10519  uzwo  12303  shftfval  14422  fsum2dlem  15117  fprod2dlem  15326  prmpwdvds  16232  quscrng  19934  chfacfscmul0  21382  chfacfpmmul0  21386  tgtop  21497  neitr  21704  bwth  21934  tx1stc  22174  cnextcn  22591  logfac2  25707  2sqmo  25927  outpasch  26455  trgcopyeu  26506  axcontlem12  26676  spanuni  29236  pjnmopi  29840  superpos  30046  atcvat4i  30089  rabeqsnd  30179  fpwrelmap  30383  locfinreflem  30991  cmpcref  31001  loop1cycl  32269  fneint  33581  neibastop3  33595  isbasisrelowllem1  34506  isbasisrelowllem2  34507  relowlssretop  34514  finxpreclem6  34547  ralssiun  34558  fin2so  34747  matunitlindflem2  34757  poimirlem26  34786  poimirlem27  34787  heicant  34795  ismblfin  34801  ovoliunnfl  34802  itg2gt0cn  34815  cvrat4  36447  pell14qrexpcl  39326  liminflimsupxrre  41960  odz2prm2pw  43554  prelrrx2b  44530
  Copyright terms: Public domain W3C validator