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

Theorem 3imp2 1279
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 1278 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
32imp 445 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  wereu  5080  ovg  6764  fisup2g  8334  fiinf2g  8366  cfcoflem  9054  ttukeylem5  9295  dedekindle  10161  grplcan  17417  mulgnnass  17516  mulgnnassOLD  17517  dmdprdsplit2  18385  mulgass2  18541  lmodvsdi  18826  lmodvsdir  18827  lmodvsass  18828  lss1d  18903  islmhm2  18978  lspsolvlem  19082  lbsextlem2  19099  cygznlem2a  19856  isphld  19939  t0dist  21069  hausnei  21072  nrmsep3  21099  fclsopni  21759  fcfneii  21781  ax5seglem5  25747  axcont  25790  grporcan  27260  grpolcan  27272  slmdvsdi  29595  slmdvsdir  29596  slmdvsass  29597  mclsppslem  31241  broutsideof2  31924  poimirlem31  33111  broucube  33114  frinfm  33201  crngm23  33472  pridl  33507  pridlc  33541  dmnnzd  33545  dmncan1  33546  paddasslem5  34629  sfprmdvdsmersenne  40849
  Copyright terms: Public domain W3C validator