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  1362  tz7.49  8072  supxrun  12699  injresinj  13148  fi1uzind  13845  brfi1indALT  13848  swrdswrdlem  14056  swrdswrd  14057  2cshwcshw  14177  cshwcsh2id  14180  prmgaplem6  16382  cusgrsize2inds  27163  usgr2pthlem  27472  usgr2pth  27473  elwwlks2  27673  rusgrnumwwlks  27681  clwlkclwwlklem2a4  27703  clwlkclwwlklem2  27706  umgrhashecclwwlk  27785  1to3vfriswmgr  27987  frgrnbnb  28000  branmfn  29810  relowlpssretop  34528  broucube  34808  eel0000  40934  eel00001  40935  eel00000  40936  eel11111  40937  climrec  41764  bgoldbtbndlem4  43820  bgoldbtbnd  43821  tgoldbach  43829  isomuspgr  43846  2zlidl  44103  2zrngmmgm  44115  lincsumcl  44384
  Copyright terms: Public domain W3C validator