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 208  df-an 397
This theorem is referenced by:  ad5ant2345  1364  tz7.49  8072  supxrun  12699  injresinj  13148  fi1uzind  13845  brfi1indALT  13848  swrdswrdlem  14056  swrdswrd  14057  2cshwcshw  14177  cshwcsh2id  14180  prmgaplem6  16382  cusgrsize2inds  27149  usgr2pthlem  27458  usgr2pth  27459  elwwlks2  27659  rusgrnumwwlks  27667  clwlkclwwlklem2a4  27689  clwlkclwwlklem2  27692  umgrhashecclwwlk  27771  1to3vfriswmgr  27973  frgrnbnb  27986  branmfn  29796  relowlpssretop  34514  broucube  34793  eel0000  40919  eel00001  40920  eel00000  40921  eel11111  40922  climrec  41749  bgoldbtbndlem4  43805  bgoldbtbnd  43806  tgoldbach  43814  isomuspgr  43831  2zlidl  44037  2zrngmmgm  44049  lincsumcl  44318
  Copyright terms: Public domain W3C validator