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  8086  sqrmo  15204  icodiamlt  15391  psgnunilem2  19461  haust1  23327  cnhaus  23329  isreg2  23352  llynlly  23452  restnlly  23457  llyrest  23460  llyidm  23463  nllyidm  23464  cldllycmp  23470  txlly  23611  txnlly  23612  pthaus  23613  txhaus  23622  txkgen  23627  xkohaus  23628  xkococnlem  23634  hauspwpwf1  23962  itg2add  25736  ulmdvlem3  26380  nosupno  27681  noinfno  27696  etaslts  27799  cutbdaybnd  27801  cutbdaybnd2  27802  addsproplem6  27980  negsproplem6  28039  mulsproplem13  28134  mulsproplem14  28135  mulsprop  28136  bdayfinbndlem1  28473  ax5seglem6  29017  fusgrfis  29413  umgr2wlkon  30033  numclwwlk5  30473  connpconn  35433  cvmliftmolem2  35480  cvmlift2lem10  35510  cvmlift3lem2  35518  cvmlift3lem8  35524  broutsideof3  36324  unblimceq0  36783  paddasslem10  40289  lhpexle2lem  40469  lhpexle3lem  40471  cdlemj3  41283  cdlemkid4  41394  mpaaeu  43596  stoweidlem35  46481  stoweidlem56  46502  stoweidlem59  46505  2arwcat  50087