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

Theorem 3expd 1347
Description: Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3expd.1 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
Assertion
Ref Expression
3expd (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem 3expd
StepHypRef Expression
1 3expd.1 . . . 4 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
21com12 32 . . 3 ((𝜓𝜒𝜃) → (𝜑𝜏))
323exp 1113 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
43com4r 94 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081
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  df-3an 1083
This theorem is referenced by:  3exp2  1348  exp516  1350  3impexp  1352  smogt  7995  axdc3lem4  9864  axcclem  9868  caubnd  14708  coprmprod  15995  catidd  16941  mulgnnass  18192  numedglnl  26843  mclsind  32701  fscgr  33425  cvrat4  36446  3dim1  36470  3dim2  36471  llnle  36521  lplnle  36543  llncvrlpln2  36560  lplncvrlvol2  36618  pmaple  36764  paddasslem14  36836  paddasslem15  36837  osumcllem11N  36969  cdlemeg46gfre  37535  cdlemk33N  37912  dia2dimlem6  38072  lclkrlem2y  38534  rexlimdv3d  39145  relexpmulnn  39919  3impexpbicom  40678  icceuelpart  43428
  Copyright terms: Public domain W3C validator