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

Theorem expl 646
 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 628 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 446 1 (𝜑 → ((𝜓𝜒) → 𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  reximd2a  2996  tfindsg2  6953  tz7.49c  7428  ssenen  8019  pssnn  8063  unwdomg  8372  cff1  8963  cfsmolem  8975  cfpwsdom  9285  wunex2  9439  mulgt0sr  9805  uzwo  11627  shftfval  13658  fsum2dlem  14343  fprod2dlem  14549  prmpwdvds  15446  quscrng  19061  chfacfscmul0  20482  chfacfpmmul0  20486  tgtop  20588  neitr  20794  bwth  21023  tx1stc  21263  cnextcn  21681  logfac2  24742  axcontlem12  25655  numclwwlkun  26606  spanuni  27787  pjnmopi  28391  superpos  28597  atcvat4i  28640  fpwrelmap  28896  2sqmo  28980  locfinreflem  29235  cmpcref  29245  fneint  31513  neibastop3  31527  isbasisrelowllem1  32379  isbasisrelowllem2  32380  relowlssretop  32387  finxpreclem6  32409  fin2so  32566  matunitlindflem2  32576  poimirlem26  32605  poimirlem27  32606  heicant  32614  ismblfin  32620  ovoliunnfl  32621  itg2gt0cn  32635  cvrat4  33747  pell14qrexpcl  36449  odz2prm2pw  40013
 Copyright terms: Public domain W3C validator