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

Theorem simp1i 1136
Description: Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
Hypothesis
Ref Expression
3simp1i.1 (𝜑𝜓𝜒)
Assertion
Ref Expression
simp1i 𝜑

Proof of Theorem simp1i
StepHypRef Expression
1 3simp1i.1 . 2 (𝜑𝜓𝜒)
2 simp1 1133 . 2 ((𝜑𝜓𝜒) → 𝜑)
31, 2ax-mp 5 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  w3a 1084
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 395  df-3an 1086
This theorem is referenced by:  find  7908  findOLD  7909  hartogslem2  9574  harwdom  9622  divalglem6  16382  structfn  17132  strleun  17133  oppcbas  17706  rescbas  17819  rescabs  17825  rmodislmod  20820  rmodislmodOLD  20821  sratset  21081  srads  21084  tngsca  24578  birthday  26906  divsqrsumf  26933  emcl  26955  lgslem4  27253  lgscllem  27257  lgsdir2lem2  27279  mulog2sumlem1  27487  siilem2  30682  h2hva  30804  h2hsm  30805  elunop2  31843  zlmds  33596  zlmtset  33598  wallispilem3  45484  wallispilem4  45485  prstcbas  48151
  Copyright terms: Public domain W3C validator