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

Theorem 3imp1 1409
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 1098 . 2 ((𝜑𝜓𝜒) → (𝜃𝜏))
32imp 397 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071
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 199  df-an 387  df-3an 1073
This theorem is referenced by:  3an1rs  1421  reupick2  4139  indcardi  9199  ledivge1le  12214  expcan  13235  ltexp2  13236  leexp1a  13241  expnbnd  13316  cshf1  13965  rtrclreclem4  14212  relexpindlem  14214  ncoprmlnprm  15844  xrsdsreclblem  20192  matecl  20639  scmateALT  20727  riinopn  21124  neindisj2  21339  filufint  22136  tsmsxp  22370  ewlkle  26957  uspgr2wlkeq  26997  spthonepeq  27108  wwlksm1edg  27234  wwlksm1edgOLD  27235  clwwisshclwws  27408  clwwlknwwlksn  27431  clwwlkinwwlk  27433  clwwlkinwwlkOLD  27434  wwlksext2clwwlk  27458  3vfriswmgr  27690  homco1  29236  homulass  29237  hoadddir  29239  mblfinlem3  34079  zerdivemp1x  34375  athgt  35615  psubspi  35906  paddasslem14  35992  eluzge0nn0  42364  iccpartigtl  42401  lighneal  42559  isomgrsym  42759
  Copyright terms: Public domain W3C validator