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

Theorem 3impd 1273
Description: Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3imp1.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
3impd (𝜑 → ((𝜓𝜒𝜃) → 𝜏))

Proof of Theorem 3impd
StepHypRef Expression
1 3imp1.1 . . . 4 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21com4l 90 . . 3 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
323imp 1249 . 2 ((𝜓𝜒𝜃) → (𝜑𝜏))
43com12 32 1 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  3imp2  1274  3impexp  1281  oprabid  6554  wfrlem12  7291  isinf  8036  axdc3lem4  9136  iccid  12050  difreicc  12134  relexpaddg  13590  issubg4  17385  reconn  22387  bcthlem2  22875  dvfsumrlim3  23545  ax5seg  25564  axcontlem4  25593  3v3e3cycl1  25966  4cycl4v4e  25988  4cycl4dv4e  25990  2spontn0vne  26208  eupai  26288  cvmlift3lem4  30352  frrlem11  30830  fscgr  31151  idinside  31155  brsegle  31179  seglecgr12im  31181  imp5q  31270  elicc3  31275  areacirclem1  32464  areacirclem2  32465  areacirclem4  32467  areacirc  32469  filbcmb  32499  fzmul  32501  islshpcv  33152  cvrat3  33540  4atexlem7  34173  relexpmulg  36815  gneispacess2  37258  iunconlem2  37987  fmtnoprmfac1  39810  fmtnoprmfac2  39812  fundmge2nop0  40142  usgr2wlkneq  40954
  Copyright terms: Public domain W3C validator