Theorem simprr1 1222

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp2  8125  sqrmo  15224  icodiamlt  15411  psgnunilem2  19432  haust1  23246  cnhaus  23248  isreg2  23271  llynlly  23371  restnlly  23376  llyrest  23379  llyidm  23382  nllyidm  23383  cldllycmp  23389  txlly  23530  txnlly  23531  pthaus  23532  txhaus  23541  txkgen  23546  xkohaus  23547  xkococnlem  23553  hauspwpwf1  23881  itg2add  25667  ulmdvlem3  26318  nosupno  27622  noinfno  27637  etasslt  27732  scutbdaybnd  27734  scutbdaybnd2  27735  addsproplem6  27888  negsproplem6  27946  mulsproplem13  28038  mulsproplem14  28039  mulsprop  28040  ax5seglem6  28868  fusgrfis  29264  umgr2wlkon  29887  numclwwlk5  30324  connpconn  35229  cvmliftmolem2  35276  cvmlift2lem10  35306  cvmlift3lem2  35314  cvmlift3lem8  35320  broutsideof3  36121  unblimceq0  36502  paddasslem10  39830  lhpexle2lem  40010  lhpexle3lem  40012  cdlemj3  40824  cdlemkid4  40935  mpaaeu  43146  stoweidlem35  46040  stoweidlem56  46061  stoweidlem59  46064  2arwcat  49593