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

Theorem 3imp1 1272
Description: Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3imp1.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
3imp1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem 3imp1
StepHypRef Expression
1 3imp1.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
213imp 1249 . 2 ((𝜑𝜓𝜒) → (𝜃𝜏))
32imp 444 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  reupick2  3872  indcardi  8747  ledivge1le  11777  expcan  12775  ltexp2  12776  leexp1a  12781  expnbnd  12855  cshf1  13407  rtrclreclem4  13649  relexpindlem  13651  ncoprmlnprm  15274  xrsdsreclblem  19611  matecl  20050  scmateALT  20137  riinopn  20538  neindisj2  20737  filufint  21534  tsmsxp  21768  spthonepeq  26117  usg2wlkeq  26236  rusgraprop4  26471  vdn0frgrav2  26550  vdn1frgrav2  26552  usgreghash2spot  26596  homco1  28044  homulass  28045  hoadddir  28047  mblfinlem3  32618  zerdivemp1x  32916  athgt  33760  psubspi  34051  paddasslem14  34137  iccpartigtl  39961  lighneal  40066  eluzge0nn0  40350  ewlkle  40807  uspgr2wlkeq  40854  spthonepeq-av  40958  wwlksm1edg  41078  clwwisshclwws  41235  3vfriswmgr  41448  av-extwwlkfablem2  41510
  Copyright terms: Public domain W3C validator