Theorem simprr1 1222

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simprr1	⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

Proof of Theorem simprr1

Step	Hyp	Ref	Expression
1		simp1 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antll 729	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

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  8079  sqrmo  15160  icodiamlt  15347  psgnunilem2  19409  haust1  23268  cnhaus  23270  isreg2  23293  llynlly  23393  restnlly  23398  llyrest  23401  llyidm  23404  nllyidm  23405  cldllycmp  23411  txlly  23552  txnlly  23553  pthaus  23554  txhaus  23563  txkgen  23568  xkohaus  23569  xkococnlem  23575  hauspwpwf1  23903  itg2add  25688  ulmdvlem3  26339  nosupno  27643  noinfno  27658  etasslt  27755  scutbdaybnd  27757  scutbdaybnd2  27758  addsproplem6  27918  negsproplem6  27976  mulsproplem13  28068  mulsproplem14  28069  mulsprop  28070  ax5seglem6  28914  fusgrfis  29310  umgr2wlkon  29930  numclwwlk5  30370  connpconn  35300  cvmliftmolem2  35347  cvmlift2lem10  35377  cvmlift3lem2  35385  cvmlift3lem8  35391  broutsideof3  36191  unblimceq0  36572  paddasslem10  39948  lhpexle2lem  40128  lhpexle3lem  40130  cdlemj3  40942  cdlemkid4  41053  mpaaeu  43267  stoweidlem35  46157  stoweidlem56  46178  stoweidlem59  46181  2arwcat  49725