Theorem simprr1 1219

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1085

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 210  df-an 401  df-3an 1087

This theorem is referenced by:  sqrmo  14660  icodiamlt  14844  psgnunilem2  18691  haust1  22053  cnhaus  22055  isreg2  22078  llynlly  22178  restnlly  22183  llyrest  22186  llyidm  22189  nllyidm  22190  cldllycmp  22196  txlly  22337  txnlly  22338  pthaus  22339  txhaus  22348  txkgen  22353  xkohaus  22354  xkococnlem  22360  hauspwpwf1  22688  itg2add  24460  ulmdvlem3  25097  ax5seglem6  26828  fusgrfis  27220  umgr2wlkon  27836  numclwwlk5  28273  connpconn  32714  cvmliftmolem2  32761  cvmlift2lem10  32791  cvmlift3lem2  32799  cvmlift3lem8  32805  poxp2  33346  nosupno  33472  noinfno  33487  etasslt  33569  scutbdaybnd  33571  scutbdaybnd2  33572  broutsideof3  33978  unblimceq0  34237  paddasslem10  37406  lhpexle2lem  37586  lhpexle3lem  37588  cdlemj3  38400  cdlemkid4  38511  mpaaeu  40468  stoweidlem35  43044  stoweidlem56  43065  stoweidlem59  43068