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

Theorem exp41 435
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp41.1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Assertion
Ref Expression
exp41 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem exp41
StepHypRef Expression
1 exp41.1 . . 3 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
21ex 413 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜃𝜏))
32exp31 420 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 206  df-an 397
This theorem is referenced by:  ad5ant2345  1369  tz7.49  8276  supxrun  13050  injresinj  13508  fi1uzind  14211  brfi1indALT  14214  swrdswrdlem  14417  swrdswrd  14418  2cshwcshw  14538  cshwcsh2id  14541  prmgaplem6  16757  cusgrsize2inds  27820  usgr2pthlem  28131  usgr2pth  28132  elwwlks2  28331  rusgrnumwwlks  28339  clwlkclwwlklem2a4  28361  clwlkclwwlklem2  28364  umgrhashecclwwlk  28442  1to3vfriswmgr  28644  frgrnbnb  28657  branmfn  30467  elrspunidl  31606  zarcmplem  31831  relowlpssretop  35535  broucube  35811  eel0000  42340  eel00001  42341  eel00000  42342  eel11111  42343  climrec  43144  bgoldbtbndlem4  45260  bgoldbtbnd  45261  tgoldbach  45269  isomuspgr  45286  2zlidl  45492  2zrngmmgm  45504  lincsumcl  45772
  Copyright terms: Public domain W3C validator