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

Theorem expl 649
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 631 . 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 197  df-an 385
This theorem is referenced by:  reximd2a  3151  tfindsg2  7226  tz7.49c  7710  ssenen  8299  pssnn  8343  unwdomg  8654  cff1  9272  cfsmolem  9284  cfpwsdom  9598  wunex2  9752  mulgt0sr  10118  uzwo  11944  shftfval  14009  fsum2dlem  14700  fprod2dlem  14909  prmpwdvds  15810  quscrng  19442  chfacfscmul0  20865  chfacfpmmul0  20869  tgtop  20979  neitr  21186  bwth  21415  tx1stc  21655  cnextcn  22072  logfac2  25141  axcontlem12  26054  spanuni  28712  pjnmopi  29316  superpos  29522  atcvat4i  29565  rabeqsnd  29649  fpwrelmap  29817  2sqmo  29958  locfinreflem  30216  cmpcref  30226  fneint  32649  neibastop3  32663  bj-ismooredr2  33371  isbasisrelowllem1  33514  isbasisrelowllem2  33515  relowlssretop  33522  finxpreclem6  33544  fin2so  33709  matunitlindflem2  33719  poimirlem26  33748  poimirlem27  33749  heicant  33757  ismblfin  33763  ovoliunnfl  33764  itg2gt0cn  33778  cvrat4  35232  pell14qrexpcl  37933  odz2prm2pw  41985
  Copyright terms: Public domain W3C validator