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

Theorem 3expd 1462
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 1148 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
43com4r 94 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  3exp2  1463  exp516  1465  3impexp  1467  smogt  7668  axdc3lem4  9528  axcclem  9532  caubnd  14383  coprmprod  15655  catidd  16606  mulgnnass  17841  numedglnl  26317  mclsind  31915  fscgr  32631  cvrat4  35399  3dim1  35423  3dim2  35424  llnle  35474  lplnle  35496  llncvrlpln2  35513  lplncvrlvol2  35571  pmaple  35717  paddasslem14  35789  paddasslem15  35790  osumcllem11N  35922  cdlemeg46gfre  36488  cdlemk33N  36865  dia2dimlem6  37025  lclkrlem2y  37487  relexpmulnn  38676  3impexpbicom  39357  icceuelpart  42106
  Copyright terms: Public domain W3C validator