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  8085  sqrmo  15174  icodiamlt  15361  psgnunilem2  19424  haust1  23296  cnhaus  23298  isreg2  23321  llynlly  23421  restnlly  23426  llyrest  23429  llyidm  23432  nllyidm  23433  cldllycmp  23439  txlly  23580  txnlly  23581  pthaus  23582  txhaus  23591  txkgen  23596  xkohaus  23597  xkococnlem  23603  hauspwpwf1  23931  itg2add  25716  ulmdvlem3  26367  nosupno  27671  noinfno  27686  etaslts  27789  cutbdaybnd  27791  cutbdaybnd2  27792  addsproplem6  27970  negsproplem6  28029  mulsproplem13  28124  mulsproplem14  28125  mulsprop  28126  bdayfinbndlem1  28463  ax5seglem6  29007  fusgrfis  29403  umgr2wlkon  30023  numclwwlk5  30463  connpconn  35429  cvmliftmolem2  35476  cvmlift2lem10  35506  cvmlift3lem2  35514  cvmlift3lem8  35520  broutsideof3  36320  unblimceq0  36707  paddasslem10  40085  lhpexle2lem  40265  lhpexle3lem  40267  cdlemj3  41079  cdlemkid4  41190  mpaaeu  43388  stoweidlem35  46275  stoweidlem56  46296  stoweidlem59  46299  2arwcat  49841