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

Theorem exp41 426
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 402 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜃𝜏))
32exp31 411 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  syl1111anc  869  ad5ant2345  1490  tz7.49  7780  supxrun  12394  injresinj  12843  fi1uzind  13527  brfi1indALT  13530  swrdswrdlem  13746  swrdswrd  13747  2cshwcshw  13909  cshwcsh2id  13912  prmgaplem6  16092  cusgrsize2inds  26702  usgr2pthlem  27016  usgr2pth  27017  wwlksnext  27161  elwwlks2  27256  rusgrnumwwlks  27264  rusgrnumwwlksOLD  27265  clwlkclwwlklem2a4  27289  clwlkclwwlklem2  27292  umgrhashecclwwlk  27395  clwlksfclwwlkOLD  27402  1to3vfriswmgr  27628  frgrnbnb  27641  branmfn  29488  relowlpssretop  33709  broucube  33931  eel0001  39710  eel0000  39711  eel00001  39712  eel00000  39713  eel11111  39714  climrec  40574  bgoldbtbndlem4  42473  bgoldbtbnd  42474  tgoldbach  42482  isomuspgr  42499  2zlidl  42728  2zrngmmgm  42740  lincsumcl  43014
  Copyright terms: Public domain W3C validator