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  8142  sqrmo  15270  icodiamlt  15454  psgnunilem2  19476  haust1  23290  cnhaus  23292  isreg2  23315  llynlly  23415  restnlly  23420  llyrest  23423  llyidm  23426  nllyidm  23427  cldllycmp  23433  txlly  23574  txnlly  23575  pthaus  23576  txhaus  23585  txkgen  23590  xkohaus  23591  xkococnlem  23597  hauspwpwf1  23925  itg2add  25712  ulmdvlem3  26363  nosupno  27667  noinfno  27682  etasslt  27777  scutbdaybnd  27779  scutbdaybnd2  27780  addsproplem6  27933  negsproplem6  27991  mulsproplem13  28083  mulsproplem14  28084  mulsprop  28085  ax5seglem6  28913  fusgrfis  29309  umgr2wlkon  29932  numclwwlk5  30369  connpconn  35257  cvmliftmolem2  35304  cvmlift2lem10  35334  cvmlift3lem2  35342  cvmlift3lem8  35348  broutsideof3  36144  unblimceq0  36525  paddasslem10  39848  lhpexle2lem  40028  lhpexle3lem  40030  cdlemj3  40842  cdlemkid4  40953  mpaaeu  43174  stoweidlem35  46064  stoweidlem56  46085  stoweidlem59  46088  2arwcat  49477