Theorem simprr1 1217

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 1132	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antll 727	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:  sqrmo  14614  icodiamlt  14798  psgnunilem2  18626  haust1  21963  cnhaus  21965  isreg2  21988  llynlly  22088  restnlly  22093  llyrest  22096  llyidm  22099  nllyidm  22100  cldllycmp  22106  txlly  22247  txnlly  22248  pthaus  22249  txhaus  22258  txkgen  22263  xkohaus  22264  xkococnlem  22270  hauspwpwf1  22598  itg2add  24363  ulmdvlem3  24993  ax5seglem6  26723  fusgrfis  27115  umgr2wlkon  27732  numclwwlk5  28170  connpconn  32486  cvmliftmolem2  32533  cvmlift2lem10  32563  cvmlift3lem2  32571  cvmlift3lem8  32577  nosupno  33207  scutbdaybnd  33279  broutsideof3  33591  unblimceq0  33850  paddasslem10  36969  lhpexle2lem  37149  lhpexle3lem  37151  cdlemj3  37963  cdlemkid4  38074  mpaaeu  39756  stoweidlem35  42327  stoweidlem56  42348  stoweidlem59  42351