Theorem simprr1 1214

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 1129	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antll 725	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  sqrmo  14449  icodiamlt  14633  psgnunilem2  18358  haust1  21648  cnhaus  21650  isreg2  21673  llynlly  21773  restnlly  21778  llyrest  21781  llyidm  21784  nllyidm  21785  cldllycmp  21791  txlly  21932  txnlly  21933  pthaus  21934  txhaus  21943  txkgen  21948  xkohaus  21949  xkococnlem  21955  hauspwpwf1  22283  itg2add  24047  ulmdvlem3  24677  ax5seglem6  26407  fusgrfis  26799  umgr2wlkon  27415  numclwwlk5  27855  connpconn  32092  cvmliftmolem2  32139  cvmlift2lem10  32169  cvmlift3lem2  32177  cvmlift3lem8  32183  nosupno  32814  scutbdaybnd  32886  broutsideof3  33198  unblimceq0  33457  paddasslem10  36517  lhpexle2lem  36697  lhpexle3lem  36699  cdlemj3  37511  cdlemkid4  37622  mpaaeu  39256  stoweidlem35  41884  stoweidlem56  41905  stoweidlem59  41908