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  8083  sqrmo  15176  icodiamlt  15363  psgnunilem2  19392  haust1  23255  cnhaus  23257  isreg2  23280  llynlly  23380  restnlly  23385  llyrest  23388  llyidm  23391  nllyidm  23392  cldllycmp  23398  txlly  23539  txnlly  23540  pthaus  23541  txhaus  23550  txkgen  23555  xkohaus  23556  xkococnlem  23562  hauspwpwf1  23890  itg2add  25676  ulmdvlem3  26327  nosupno  27631  noinfno  27646  etasslt  27742  scutbdaybnd  27744  scutbdaybnd2  27745  addsproplem6  27904  negsproplem6  27962  mulsproplem13  28054  mulsproplem14  28055  mulsprop  28056  ax5seglem6  28897  fusgrfis  29293  umgr2wlkon  29913  numclwwlk5  30350  connpconn  35207  cvmliftmolem2  35254  cvmlift2lem10  35284  cvmlift3lem2  35292  cvmlift3lem8  35298  broutsideof3  36099  unblimceq0  36480  paddasslem10  39808  lhpexle2lem  39988  lhpexle3lem  39990  cdlemj3  40802  cdlemkid4  40913  mpaaeu  43123  stoweidlem35  46017  stoweidlem56  46038  stoweidlem59  46041  2arwcat  49586