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

Theorem 3imp1 1341
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 1105 . 2 ((𝜑𝜓𝜒) → (𝜃𝜏))
32imp 409 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1081
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 209  df-an 399  df-3an 1083
This theorem is referenced by:  3an1rs  1353  reupick2  4287  indcardi  9459  ledivge1le  12452  expcan  13525  ltexp2  13526  leexp1a  13531  expnbnd  13585  cshf1  14164  rtrclreclem4  14412  relexpindlem  14414  ncoprmlnprm  16060  xrsdsreclblem  20583  matecl  21026  scmateALT  21113  riinopn  21508  neindisj2  21723  filufint  22520  tsmsxp  22755  ewlkle  27379  uspgr2wlkeq  27419  spthonepeq  27525  wwlksm1edg  27651  clwwisshclwws  27785  clwwlknwwlksn  27808  clwwlkinwwlk  27810  wwlksext2clwwlk  27828  3vfriswmgr  28049  homco1  29570  homulass  29571  hoadddir  29573  satffunlem  32636  mblfinlem3  34913  zerdivemp1x  35207  athgt  36574  psubspi  36865  paddasslem14  36951  eluzge0nn0  43492  iccpartigtl  43563  lighneal  43756  isomgrsym  43981
  Copyright terms: Public domain W3C validator