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

Theorem 3expd 1408
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 1112 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
43com4r 94 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  3exp2  1409  exp516  1411  3impexp  1413  smogt  7584  axdc3lem4  9388  axcclem  9392  caubnd  14218  coprmprod  15498  catidd  16463  mulgnnass  17698  mulgnnassOLD  17699  numedglnl  26159  mclsind  31695  fscgr  32414  cvrat4  35149  3dim1  35173  3dim2  35174  llnle  35224  lplnle  35246  llncvrlpln2  35263  lplncvrlvol2  35321  pmaple  35467  paddasslem14  35539  paddasslem15  35540  osumcllem11N  35672  cdlemeg46gfre  36239  cdlemk33N  36616  dia2dimlem6  36777  lclkrlem2y  37239  relexpmulnn  38420  3impexpbicom  39104  icceuelpart  41799
  Copyright terms: Public domain W3C validator