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

Theorem expl 645
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 627 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 445 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  reximd2a  2995  tfindsg2  6930  tz7.49c  7405  ssenen  7996  pssnn  8040  unwdomg  8349  cff1  8940  cfsmolem  8952  cfpwsdom  9262  wunex2  9416  mulgt0sr  9782  uzwo  11583  shftfval  13604  fsum2dlem  14289  fprod2dlem  14495  prmpwdvds  15392  quscrng  19007  chfacfscmul0  20424  chfacfpmmul0  20428  tgtop  20530  neitr  20736  bwth  20965  tx1stc  21205  cnextcn  21623  logfac2  24659  axcontlem12  25573  numclwwlkun  26372  spanuni  27593  pjnmopi  28197  superpos  28403  atcvat4i  28446  fpwrelmap  28702  2sqmo  28786  locfinreflem  29041  cmpcref  29051  fneint  31319  neibastop3  31333  isbasisrelowllem1  32182  isbasisrelowllem2  32183  relowlssretop  32190  finxpreclem6  32212  fin2so  32369  matunitlindflem2  32379  poimirlem26  32408  poimirlem27  32409  heicant  32417  ismblfin  32423  ovoliunnfl  32424  itg2gt0cn  32438  cvrat4  33550  pell14qrexpcl  36252  odz2prm2pw  39818
  Copyright terms: Public domain W3C validator