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

Theorem 3expd 1354
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 1120 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
43com4r 94 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  3exp2  1355  exp516  1357  3impexp  1359  smogt  8407  axdc3lem4  10493  axcclem  10497  caubnd  15397  coprmprod  16698  catidd  17723  mulgnnass  19127  numedglnl  29161  mclsind  35575  fscgr  36081  cvrat4  39445  3dim1  39469  3dim2  39470  llnle  39520  lplnle  39542  llncvrlpln2  39559  lplncvrlvol2  39617  pmaple  39763  paddasslem14  39835  paddasslem15  39836  osumcllem11N  39968  cdlemeg46gfre  40534  cdlemk33N  40911  dia2dimlem6  41071  lclkrlem2y  41533  rexlimdv3d  42694  relexpmulnn  43722  3impexpbicom  44500  icceuelpart  47423  grlimgrtri  47963
  Copyright terms: Public domain W3C validator