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

Theorem 3expd 1282
 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 1262 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
43com4r 94 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1036 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  df-3an 1038 This theorem is referenced by:  3exp2  1283  exp516  1285  3impexp  1287  smogt  7449  axdc3lem4  9260  axcclem  9264  caubnd  14079  coprmprod  15356  catidd  16322  mulgnnass  17557  mulgnnassOLD  17558  numedglnl  26020  mclsind  31441  fscgr  32162  cvrat4  34548  3dim1  34572  3dim2  34573  llnle  34623  lplnle  34645  llncvrlpln2  34662  lplncvrlvol2  34720  pmaple  34866  paddasslem14  34938  paddasslem15  34939  osumcllem11N  35071  cdlemeg46gfre  35639  cdlemk33N  36016  dia2dimlem6  36177  lclkrlem2y  36639  relexpmulnn  37820  3impexpbicom  38505  icceuelpart  41136
 Copyright terms: Public domain W3C validator