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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3imp2  1346  3impexp  1355  po2ne  5457  oprabidw  7170  oprabid  7171  wfrlem12  7953  isinf  8719  infsupprpr  8956  axdc3lem4  9868  iccid  12775  difreicc  12866  relexpaddg  14407  issubg4  18293  reconn  23436  bcthlem2  23932  dvfsumrlim3  24639  ax5seg  26735  axcontlem4  26764  usgr2wlkneq  27548  frgrwopreg  28111  cvmlift3lem4  32677  fscgr  33649  idinside  33653  brsegle  33677  seglecgr12im  33679  imp5q  33768  elicc3  33773  areacirclem1  35138  areacirclem2  35139  areacirclem4  35141  areacirc  35143  filbcmb  35171  fzmul  35172  islshpcv  36342  cvrat3  36731  4atexlem7  37364  relexpmulg  40398  gneispacess2  40836  iunconnlem2  41628  fmtnoprmfac1  44069  fmtnoprmfac2  44071  fpprwppr  44244  itsclc0xyqsol  45169
  Copyright terms: Public domain W3C validator