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

Theorem 3imp1 1348
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 1111 . 2 ((𝜑𝜓𝜒) → (𝜃𝜏))
32imp 406 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  3an1rs  1360  reupick2  4331  indcardi  10081  ledivge1le  13106  expcan  14209  ltexp2  14210  leexp1a  14215  expnbnd  14271  cshf1  14848  rtrclreclem4  15100  relexpindlem  15102  ncoprmlnprm  16765  rnglidlmcl  21226  xrsdsreclblem  21430  matecl  22431  scmateALT  22518  riinopn  22914  neindisj2  23131  filufint  23928  tsmsxp  24163  ewlkle  29623  uspgr2wlkeq  29664  spthonepeq  29772  wwlksm1edg  29901  clwwisshclwws  30034  clwwlknwwlksn  30057  clwwlkinwwlk  30059  wwlksext2clwwlk  30076  3vfriswmgr  30297  homco1  31820  homulass  31821  hoadddir  31823  satffunlem  35406  mblfinlem3  37666  zerdivemp1x  37954  athgt  39458  psubspi  39749  paddasslem14  39835  eluzge0nn0  47324  iccpartigtl  47410  lighneal  47598  uhgrimisgrgriclem  47898  uhgrimisgrgric  47899  clnbgrgrimlem  47901  uspgrlimlem3  47957  clnbgr3stgrgrlic  47979  gpgusgralem  48011
  Copyright terms: Public domain W3C validator