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

Theorem 3imp2 1341
Description: Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3imp1.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
3imp2 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)

Proof of Theorem 3imp2
StepHypRef Expression
1 3imp1.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
213impd 1340 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
32imp 407 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  wereu  5544  ovg  7302  fisup2g  8920  fiinf2g  8952  cfcoflem  9682  ttukeylem5  9923  dedekindle  10792  grplcan  18099  mulgnnass  18200  dmdprdsplit2  19097  mulgass2  19280  lmodvsdi  19586  lmodvsdir  19587  lmodvsass  19588  lss1d  19664  islmhm2  19739  lspsolvlem  19843  lbsextlem2  19860  cygznlem2a  20642  isphld  20726  t0dist  21861  hausnei  21864  nrmsep3  21891  fclsopni  22551  fcfneii  22573  ax5seglem5  26646  axcont  26689  grporcan  28222  grpolcan  28234  slmdvsdi  30770  slmdvsdir  30771  slmdvsass  30772  mclsppslem  32727  broutsideof2  33480  poimirlem31  34804  broucube  34807  frinfm  34891  crngm23  35161  pridl  35196  pridlc  35230  dmnnzd  35234  dmncan1  35235  paddasslem5  36840  or2expropbi  43146  elsetpreimafveqfv  43429  sfprmdvdsmersenne  43645
  Copyright terms: Public domain W3C validator