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

Theorem 3imp2 1350
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 1349 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
32imp 408 1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  wereu  5630  ovg  7520  fisup2g  9409  fiinf2g  9441  cfcoflem  10213  ttukeylem5  10454  dedekindle  11324  grplcan  18814  mulgnnass  18916  dmdprdsplit2  19830  mulgass2  20030  lmodvsdi  20360  lmodvsdir  20361  lmodvsass  20362  lss1d  20439  islmhm2  20514  lspsolvlem  20619  lbsextlem2  20636  cygznlem2a  20990  isphld  21074  t0dist  22692  hausnei  22695  nrmsep3  22722  fclsopni  23382  fcfneii  23404  ax5seglem5  27924  axcont  27967  grporcan  29502  grpolcan  29514  slmdvsdi  32099  slmdvsdir  32100  slmdvsass  32101  elrspunidl  32251  zarcmplem  32519  mclsppslem  34234  broutsideof2  34753  poimirlem31  36155  broucube  36158  frinfm  36240  crngm23  36507  pridl  36542  pridlc  36576  dmnnzd  36580  dmncan1  36581  paddasslem5  38333  or2expropbi  45354  elsetpreimafveqfv  45670  sfprmdvdsmersenne  45881
  Copyright terms: Public domain W3C validator