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

Theorem 3impd 1345
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 92 . . 3 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
323imp 1108 . 2 ((𝜓𝜒𝜃) → (𝜑𝜏))
43com12 32 1 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 206  df-an 395  df-3an 1086
This theorem is referenced by:  3imp2  1346  3impexp  1355  po2ne  5606  oprabidw  7450  oprabid  7451  wfrlem12OLD  8341  isinf  9285  isinfOLD  9286  infsupprpr  9529  axdc3lem4  10478  iccid  13404  difreicc  13496  relexpaddg  15036  issubg4  19108  rnglidlmcl  21124  reconn  24788  bcthlem2  25297  dvfsumrlim3  26012  ax5seg  28821  axcontlem4  28850  usgr2wlkneq  29642  frgrwopreg  30205  dfufd2lem  33361  cvmlift3lem4  35060  fscgr  35804  idinside  35808  brsegle  35832  seglecgr12im  35834  imp5q  35924  elicc3  35929  areacirclem1  37309  areacirclem2  37310  areacirclem4  37312  areacirc  37314  filbcmb  37341  fzmul  37342  islshpcv  38652  cvrat3  39042  4atexlem7  39675  relexpmulg  43279  gneispacess2  43715  iunconnlem2  44513  fmtnoprmfac1  47039  fmtnoprmfac2  47041  fpprwppr  47213  itsclc0xyqsol  48024
  Copyright terms: Public domain W3C validator