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

Theorem exp41 637
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 450 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜃𝜏))
32exp31 629 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  ad5ant2345  1314  tz7.49  7486  supxrun  12086  injresinj  12526  fi1uzind  13213  brfi1indALT  13216  fi1uzindOLD  13219  brfi1indALTOLD  13222  swrdswrdlem  13392  swrdswrd  13393  2cshwcshw  13503  cshwcsh2id  13506  prmgaplem6  15679  cusgrsize2inds  26230  usgr2pthlem  26522  usgr2pth  26523  wwlksnext  26651  elwwlks2  26722  rusgrnumwwlks  26730  clwlkclwwlklem2a4  26759  clwlkclwwlklem2  26762  umgrhashecclwwlk  26815  clwlksfclwwlk  26822  1to3vfriswmgr  27002  frgrnbnb  27015  frgrwopreg  27038  numclwwlkovf2ex  27069  branmfn  28804  relowlpssretop  32836  broucube  33061  eel0001  38413  eel0000  38414  eel1111  38415  eel00001  38416  eel00000  38417  eel11111  38418  climrec  39226  bgoldbtbndlem4  40973  bgoldbtbnd  40974  tgoldbach  40981  tgoldbachOLD  40988  2zlidl  41195  2zrngmmgm  41207  lincsumcl  41482
  Copyright terms: Public domain W3C validator