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

Theorem expl 461
 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 423 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 414 1 (𝜑 → ((𝜓𝜒) → 𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  reximd2a  3236  tfindsg2  7580  tz7.49c  8097  ssenen  8718  pssnn  8743  unfi  8746  pssnnOLD  8779  unwdomg  9086  cff1  9723  cfsmolem  9735  cfpwsdom  10049  wunex2  10203  mulgt0sr  10570  uzwo  12356  shftfval  14482  fsum2dlem  15178  fprod2dlem  15387  prmpwdvds  16300  quscrng  20086  chfacfscmul0  21563  chfacfpmmul0  21567  tgtop  21678  neitr  21885  bwth  22115  tx1stc  22355  cnextcn  22772  logfac2  25905  2sqmo  26125  outpasch  26653  trgcopyeu  26704  axcontlem12  26873  spanuni  29431  pjnmopi  30035  superpos  30241  atcvat4i  30284  rabeqsnd  30375  2ndresdju  30513  fpwrelmap  30596  nsgqusf1olem2  31124  ssmxidl  31167  locfinreflem  31315  cmpcref  31325  loop1cycl  32619  fneint  34112  neibastop3  34126  isbasisrelowllem1  35078  isbasisrelowllem2  35079  relowlssretop  35086  finxpreclem6  35119  ralssiun  35130  fin2so  35350  matunitlindflem2  35360  poimirlem26  35389  poimirlem27  35390  heicant  35398  ismblfin  35404  ovoliunnfl  35405  itg2gt0cn  35418  cvrat4  37045  pell14qrexpcl  40209  liminflimsupxrre  42853  odz2prm2pw  44476  prelrrx2b  45521  opnneilv  45620
 Copyright terms: Public domain W3C validator