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  14605  icodiamlt  14789  psgnunilem2  18617  haust1  21954  cnhaus  21956  isreg2  21979  llynlly  22079  restnlly  22084  llyrest  22087  llyidm  22090  nllyidm  22091  cldllycmp  22097  txlly  22238  txnlly  22239  pthaus  22240  txhaus  22249  txkgen  22254  xkohaus  22255  xkococnlem  22261  hauspwpwf1  22589  itg2add  24354  ulmdvlem3  24984  ax5seglem6  26714  fusgrfis  27106  umgr2wlkon  27723  numclwwlk5  28161  connpconn  32477  cvmliftmolem2  32524  cvmlift2lem10  32554  cvmlift3lem2  32562  cvmlift3lem8  32568  nosupno  33198  scutbdaybnd  33270  broutsideof3  33582  unblimceq0  33841  paddasslem10  36959  lhpexle2lem  37139  lhpexle3lem  37141  cdlemj3  37953  cdlemkid4  38064  mpaaeu  39743  stoweidlem35  42313  stoweidlem56  42334  stoweidlem59  42337