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  6576  wfrlem12  7313  isinf  8058  axdc3lem4  9158  iccid  12091  difreicc  12175  fundmge2nop0  13129  relexpaddg  13641  issubg4  17436  reconn  22439  bcthlem2  22930  dvfsumrlim3  23600  ax5seg  25618  axcontlem4  25647  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  2spontn0vne  26414  eupai  26494  cvmlift3lem4  30558  frrlem11  31036  fscgr  31357  idinside  31361  brsegle  31385  seglecgr12im  31387  imp5q  31476  elicc3  31481  areacirclem1  32670  areacirclem2  32671  areacirclem4  32673  areacirc  32675  filbcmb  32705  fzmul  32707  islshpcv  33358  cvrat3  33746  4atexlem7  34379  relexpmulg  37021  gneispacess2  37464  iunconlem2  38193  fmtnoprmfac1  40015  fmtnoprmfac2  40017  usgr2wlkneq  40962
 Copyright terms: Public domain W3C validator