Theorem simprr1 1240

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8144  sqrmo  15398  icodiamlt  15585  psgnunilem2  19689  haust1  23650  cnhaus  23652  isreg2  23675  llynlly  23776  restnlly  23781  llyrest  23784  llyidm  23787  nllyidm  23788  cldllycmp  23794  txlly  23935  txnlly  23936  pthaus  23937  txhaus  23946  txkgen  23951  xkohaus  23952  xkococnlem  23958  hauspwpwf1  24286  itg2add  26060  ulmdvlem3  26711  nosupno  28042  noinfno  28057  etaslts  28161  cutbdaybnd  28163  cutbdaybnd2  28164  addsproplem6  28342  negsproplem6  28401  mulsproplem13  28496  mulsproplem14  28497  mulsprop  28498  bdayfinbndlem1  28835  ax5seglem6  29494  fusgrfis  29893  umgr2wlkon  30521  numclwwlk5  30971  connpconn  35969  cvmliftmolem2  36016  cvmlift2lem10  36046  cvmlift3lem2  36054  cvmlift3lem8  36060  broutsideof3  36861  unblimceq0  37343  paddasslem10  40854  lhpexle2lem  41034  lhpexle3lem  41036  cdlemj3  41848  cdlemkid4  41959  mpaaeu  44110  stoweidlem35  46989  stoweidlem56  47010  stoweidlem59  47013  2arwcat  50652