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

Theorem exp41 438
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 416 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜃𝜏))
32exp31 423 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:  ad5ant2345  1371  tz7.49  8122  supxrun  12804  injresinj  13261  fi1uzind  13961  brfi1indALT  13964  swrdswrdlem  14167  swrdswrd  14168  2cshwcshw  14288  cshwcsh2id  14291  prmgaplem6  16504  cusgrsize2inds  27407  usgr2pthlem  27716  usgr2pth  27717  elwwlks2  27916  rusgrnumwwlks  27924  clwlkclwwlklem2a4  27946  clwlkclwwlklem2  27949  umgrhashecclwwlk  28027  1to3vfriswmgr  28229  frgrnbnb  28242  branmfn  30052  elrspunidl  31190  zarcmplem  31415  relowlpssretop  35190  broucube  35466  eel0000  41918  eel00001  41919  eel00000  41920  eel11111  41921  climrec  42726  bgoldbtbndlem4  44841  bgoldbtbnd  44842  tgoldbach  44850  isomuspgr  44867  2zlidl  45073  2zrngmmgm  45085  lincsumcl  45353
  Copyright terms: Public domain W3C validator