Theorem simprr1 1223

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

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

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 1089

This theorem is referenced by:  poxp2  8095  sqrmo  15186  icodiamlt  15373  psgnunilem2  19436  haust1  23308  cnhaus  23310  isreg2  23333  llynlly  23433  restnlly  23438  llyrest  23441  llyidm  23444  nllyidm  23445  cldllycmp  23451  txlly  23592  txnlly  23593  pthaus  23594  txhaus  23603  txkgen  23608  xkohaus  23609  xkococnlem  23615  hauspwpwf1  23943  itg2add  25728  ulmdvlem3  26379  nosupno  27683  noinfno  27698  etaslts  27801  cutbdaybnd  27803  cutbdaybnd2  27804  addsproplem6  27982  negsproplem6  28041  mulsproplem13  28136  mulsproplem14  28137  mulsprop  28138  bdayfinbndlem1  28475  ax5seglem6  29019  fusgrfis  29415  umgr2wlkon  30035  numclwwlk5  30475  connpconn  35448  cvmliftmolem2  35495  cvmlift2lem10  35525  cvmlift3lem2  35533  cvmlift3lem8  35539  broutsideof3  36339  unblimceq0  36726  paddasslem10  40199  lhpexle2lem  40379  lhpexle3lem  40381  cdlemj3  41193  cdlemkid4  41304  mpaaeu  43501  stoweidlem35  46387  stoweidlem56  46408  stoweidlem59  46411  2arwcat  49953