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

Theorem 3expd 1275
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 1255 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
43com4r 91 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3exp2  1276  exp516  1278  3impexp  1280  smogt  7323  axdc3lem4  9130  axcclem  9134  caubnd  13887  coprmprod  15154  catidd  16105  mulgnnass  17340  mulgnnassOLD  17341  mclsind  30522  fscgr  31158  cvrat4  33545  3dim1  33569  3dim2  33570  llnle  33620  lplnle  33642  llncvrlpln2  33659  lplncvrlvol2  33717  pmaple  33863  paddasslem14  33935  paddasslem15  33936  osumcllem11N  34068  cdlemeg46gfre  34636  cdlemk33N  35013  dia2dimlem6  35174  lclkrlem2y  35636  relexpmulnn  36818  3impexpbicom  37504  icceuelpart  39774
  Copyright terms: Public domain W3C validator