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  3312  tfindsg2  7564  tz7.49c  8073  ssenen  8680  pssnn  8725  unwdomg  9037  cff1  9669  cfsmolem  9681  cfpwsdom  9995  wunex2  10149  mulgt0sr  10516  uzwo  12300  shftfval  14419  fsum2dlem  15115  fprod2dlem  15324  prmpwdvds  16230  quscrng  19943  chfacfscmul0  21396  chfacfpmmul0  21400  tgtop  21511  neitr  21718  bwth  21948  tx1stc  22188  cnextcn  22605  logfac2  25721  2sqmo  25941  outpasch  26469  trgcopyeu  26520  axcontlem12  26689  spanuni  29249  pjnmopi  29853  superpos  30059  atcvat4i  30102  rabeqsnd  30192  fpwrelmap  30396  locfinreflem  31004  cmpcref  31014  loop1cycl  32282  fneint  33594  neibastop3  33608  isbasisrelowllem1  34519  isbasisrelowllem2  34520  relowlssretop  34527  finxpreclem6  34560  ralssiun  34571  fin2so  34761  matunitlindflem2  34771  poimirlem26  34800  poimirlem27  34801  heicant  34809  ismblfin  34815  ovoliunnfl  34816  itg2gt0cn  34829  cvrat4  36461  pell14qrexpcl  39344  liminflimsupxrre  41978  odz2prm2pw  43572  prelrrx2b  44599
  Copyright terms: Public domain W3C validator