Theorem simpr2l 1228

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

Step	Hyp	Ref	Expression
1		simprl 769	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr2 1185	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 1085

This theorem is referenced by:  oppccatid  16991  subccatid  17118  setccatid  17346  catccatid  17364  estrccatid  17384  xpccatid  17440  gsmsymgreqlem1  18560  kerf1ghm  19499  kerf1hrmOLD  19500  nllyidm  22099  ax5seg  26726  3pthdlem1  27945  segconeq  33473  ifscgr  33507  brofs2  33540  brifs2  33541  idinside  33547  btwnconn1lem8  33557  btwnconn1lem12  33561  segcon2  33568  segletr  33577  outsidele  33595  unbdqndv2  33852  lplnexllnN  36702  paddasslem9  36966  pmodlem2  36985  lhp2lt  37139  cdlemc3  37331  cdlemc4  37332  cdlemd1  37336  cdleme3b  37367  cdleme3c  37368  cdleme42ke  37623  cdlemg4c  37750