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

Theorem exp41 436
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 414 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜃𝜏))
32exp31 421 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 398
This theorem is referenced by:  ad5ant2345  1371  tz7.49  8445  supxrun  13295  injresinj  13753  fi1uzind  14458  brfi1indALT  14461  swrdswrdlem  14654  swrdswrd  14655  2cshwcshw  14776  cshwcsh2id  14779  prmgaplem6  16989  cusgrsize2inds  28710  usgr2pthlem  29020  usgr2pth  29021  elwwlks2  29220  rusgrnumwwlks  29228  clwlkclwwlklem2a4  29250  clwlkclwwlklem2  29253  umgrhashecclwwlk  29331  1to3vfriswmgr  29533  frgrnbnb  29546  branmfn  31358  elrspunidl  32546  zarcmplem  32861  relowlpssretop  36245  broucube  36522  eel0000  43481  eel00001  43482  eel00000  43483  eel11111  43484  climrec  44319  bgoldbtbndlem4  46476  bgoldbtbnd  46477  tgoldbach  46485  isomuspgr  46502  2zlidl  46832  2zrngmmgm  46844  lincsumcl  47112
  Copyright terms: Public domain W3C validator