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

Theorem 3imp2 1273
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 1272 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
32imp 443 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  wereu  5021  ovg  6672  fisup2g  8231  fiinf2g  8263  cfcoflem  8951  ttukeylem5  9192  dedekindle  10049  grplcan  17243  mulgnnass  17342  mulgnnassOLD  17343  dmdprdsplit2  18211  mulgass2  18367  lmodvsdi  18652  lmodvsdir  18653  lmodvsass  18654  lss1d  18727  islmhm2  18802  lspsolvlem  18906  lbsextlem2  18923  cygznlem2a  19677  isphld  19760  t0dist  20878  hausnei  20881  nrmsep3  20908  fclsopni  21568  fcfneii  21590  ax5seglem5  25528  axcont  25571  grporcan  26519  grpolcan  26531  slmdvsdi  28902  slmdvsdir  28903  slmdvsass  28904  mclsppslem  30537  broutsideof2  31202  poimirlem31  32410  broucube  32413  frinfm  32500  crngm23  32771  pridl  32806  pridlc  32840  dmnnzd  32844  dmncan1  32845  paddasslem5  33928  sfprmdvdsmersenne  39860
  Copyright terms: Public domain W3C validator