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  5545  ovg  7302  fisup2g  8921  fiinf2g  8953  cfcoflem  9683  ttukeylem5  9924  dedekindle  10793  grplcan  18101  mulgnnass  18202  dmdprdsplit2  19099  mulgass2  19282  lmodvsdi  19588  lmodvsdir  19589  lmodvsass  19590  lss1d  19666  islmhm2  19741  lspsolvlem  19845  lbsextlem2  19862  cygznlem2a  20644  isphld  20728  t0dist  21863  hausnei  21866  nrmsep3  21893  fclsopni  22553  fcfneii  22575  ax5seglem5  26647  axcont  26690  grporcan  28223  grpolcan  28235  slmdvsdi  30771  slmdvsdir  30772  slmdvsass  30773  mclsppslem  32728  broutsideof2  33481  poimirlem31  34805  broucube  34808  frinfm  34893  crngm23  35163  pridl  35198  pridlc  35232  dmnnzd  35236  dmncan1  35237  paddasslem5  36842  or2expropbi  43150  sfprmdvdsmersenne  43615
  Copyright terms: Public domain W3C validator