Theorem simprr1 1220

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 1135	. 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  8166  sqrmo  15286  icodiamlt  15470  psgnunilem2  19527  haust1  23375  cnhaus  23377  isreg2  23400  llynlly  23500  restnlly  23505  llyrest  23508  llyidm  23511  nllyidm  23512  cldllycmp  23518  txlly  23659  txnlly  23660  pthaus  23661  txhaus  23670  txkgen  23675  xkohaus  23676  xkococnlem  23682  hauspwpwf1  24010  itg2add  25808  ulmdvlem3  26459  nosupno  27762  noinfno  27777  etasslt  27872  scutbdaybnd  27874  scutbdaybnd2  27875  addsproplem6  28021  negsproplem6  28079  mulsproplem13  28168  mulsproplem14  28169  mulsprop  28170  ax5seglem6  28963  fusgrfis  29361  umgr2wlkon  29979  numclwwlk5  30416  connpconn  35219  cvmliftmolem2  35266  cvmlift2lem10  35296  cvmlift3lem2  35304  cvmlift3lem8  35310  broutsideof3  36107  unblimceq0  36489  paddasslem10  39811  lhpexle2lem  39991  lhpexle3lem  39993  cdlemj3  40805  cdlemkid4  40916  mpaaeu  43138  stoweidlem35  45990  stoweidlem56  46011  stoweidlem59  46014