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

Theorem expl 449
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 410 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 398 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff setvar class
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 198  df-an 385
This theorem is referenced by:  reximd2a  3158  tfindsg2  7258  tz7.49c  7744  ssenen  8340  pssnn  8384  unwdomg  8695  cff1  9332  cfsmolem  9344  cfpwsdom  9658  wunex2  9812  mulgt0sr  10178  uzwo  11951  shftfval  14096  fsum2dlem  14787  fprod2dlem  14994  prmpwdvds  15888  quscrng  19513  chfacfscmul0  20941  chfacfpmmul0  20945  tgtop  21056  neitr  21263  bwth  21492  tx1stc  21732  cnextcn  22149  logfac2  25232  axcontlem12  26145  spanuni  28793  pjnmopi  29397  superpos  29603  atcvat4i  29646  rabeqsnd  29725  fpwrelmap  29891  2sqmo  30030  locfinreflem  30288  cmpcref  30298  fneint  32717  neibastop3  32731  bj-ismooredr2  33425  isbasisrelowllem1  33568  isbasisrelowllem2  33569  relowlssretop  33576  finxpreclem6  33598  fin2so  33752  matunitlindflem2  33762  poimirlem26  33791  poimirlem27  33792  heicant  33800  ismblfin  33806  ovoliunnfl  33807  itg2gt0cn  33820  cvrat4  35331  pell14qrexpcl  38041  odz2prm2pw  42083
  Copyright terms: Public domain W3C validator