Theorem simprr1 1272

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  sqrmo  14199  icodiamlt  14381  psgnunilem2  18121  haust1  21376  cnhaus  21378  isreg2  21401  llynlly  21500  restnlly  21505  llyrest  21508  llyidm  21511  nllyidm  21512  cldllycmp  21518  txlly  21659  txnlly  21660  pthaus  21661  txhaus  21670  txkgen  21675  xkohaus  21676  xkococnlem  21682  hauspwpwf1  22010  itg2add  23745  ulmdvlem3  24375  ax5seglem6  26034  fusgrfis  26444  umgr2wlkon  27096  numclwwlk5  27584  connpconn  31552  cvmliftmolem2  31599  cvmlift2lem10  31629  cvmlift3lem2  31637  cvmlift3lem8  31643  nosupno  32183  scutbdaybnd  32255  broutsideof3  32567  unblimceq0  32832  paddasslem10  35633  lhpexle2lem  35813  lhpexle3lem  35815  cdlemj3  36628  cdlemkid4  36739  mpaaeu  38242  stoweidlem35  40765  stoweidlem56  40786  stoweidlem59  40789