Theorem simprr1 1239

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  poxp2  8137  sqrmo  15309  icodiamlt  15496  psgnunilem2  19571  haust1  23520  cnhaus  23522  isreg2  23545  llynlly  23645  restnlly  23650  llyrest  23653  llyidm  23656  nllyidm  23657  cldllycmp  23663  txlly  23804  txnlly  23805  pthaus  23806  txhaus  23815  txkgen  23820  xkohaus  23821  xkococnlem  23827  hauspwpwf1  24155  itg2add  25929  ulmdvlem3  26576  nosupno  27878  noinfno  27893  etaslts  27997  cutbdaybnd  27999  cutbdaybnd2  28000  addsproplem6  28178  negsproplem6  28237  mulsproplem13  28332  mulsproplem14  28333  mulsprop  28334  bdayfinbndlem1  28671  ax5seglem6  29295  fusgrfis  29691  umgr2wlkon  30310  numclwwlk5  30750  connpconn  35735  cvmliftmolem2  35782  cvmlift2lem10  35812  cvmlift3lem2  35820  cvmlift3lem8  35826  broutsideof3  36626  unblimceq0  37124  paddasslem10  40631  lhpexle2lem  40811  lhpexle3lem  40813  cdlemj3  41625  cdlemkid4  41736  mpaaeu  43905  stoweidlem35  46777  stoweidlem56  46798  stoweidlem59  46801  2arwcat  50406