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

Theorem simpr2l 1232
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)
Assertion
Ref Expression
simpr2l ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)

Proof of Theorem simpr2l
StepHypRef Expression
1 simprl 770 . 2 ((𝜏 ∧ (𝜑𝜓)) → 𝜑)
213ad2antr2 1189 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 1088
This theorem is referenced by:  poxp2  8169  ttrcltr  9757  ttrclss  9761  dmttrcl  9762  ttrclselem2  9767  oppccatid  17763  subccatid  17892  setccatid  18130  catccatid  18152  estrccatid  18177  xpccatid  18234  kerf1ghm  19266  gsmsymgreqlem1  19449  nllyidm  23498  noinfbnd1lem5  27773  ax5seg  28954  3pthdlem1  30184  segconeq  36012  ifscgr  36046  brofs2  36079  brifs2  36080  idinside  36086  btwnconn1lem8  36096  btwnconn1lem12  36100  segcon2  36107  segletr  36116  outsidele  36134  unbdqndv2  36513  lplnexllnN  39567  paddasslem9  39831  pmodlem2  39850  lhp2lt  40004  cdlemc3  40196  cdlemc4  40197  cdlemd1  40201  cdleme3b  40232  cdleme3c  40233  cdleme42ke  40488  cdlemg4c  40615  clnbgrgrimlem  47906  isthincd2  49111  mndtccatid  49239
  Copyright terms: Public domain W3C validator