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

Theorem exp41 434
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 412 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜃𝜏))
32exp31 419 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  ad5ant2345  1372  tz7.49  8485  supxrun  13358  injresinj  13827  fi1uzind  14546  brfi1indALT  14549  swrdswrdlem  14742  swrdswrd  14743  2cshwcshw  14864  cshwcsh2id  14867  prmgaplem6  17094  cusgrsize2inds  29471  usgr2pthlem  29783  usgr2pth  29784  elwwlks2  29986  rusgrnumwwlks  29994  clwlkclwwlklem2a4  30016  clwlkclwwlklem2  30019  umgrhashecclwwlk  30097  1to3vfriswmgr  30299  frgrnbnb  30312  branmfn  32124  elrspunidl  33456  dfufd2lem  33577  zarcmplem  33880  relowlpssretop  37365  broucube  37661  eel0000  44740  eel00001  44741  eel00000  44742  eel11111  44743  climrec  45618  bgoldbtbndlem4  47795  bgoldbtbnd  47796  tgoldbach  47804  2zlidl  48156  2zrngmmgm  48168  lincsumcl  48348
  Copyright terms: Public domain W3C validator