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  8087  sqrmo  15178  icodiamlt  15365  psgnunilem2  19428  haust1  23300  cnhaus  23302  isreg2  23325  llynlly  23425  restnlly  23430  llyrest  23433  llyidm  23436  nllyidm  23437  cldllycmp  23443  txlly  23584  txnlly  23585  pthaus  23586  txhaus  23595  txkgen  23600  xkohaus  23601  xkococnlem  23607  hauspwpwf1  23935  itg2add  25720  ulmdvlem3  26371  nosupno  27675  noinfno  27690  etasslt  27791  scutbdaybnd  27793  scutbdaybnd2  27794  addsproplem6  27956  negsproplem6  28015  mulsproplem13  28110  mulsproplem14  28111  mulsprop  28112  bdayfinbndlem1  28446  ax5seglem6  28990  fusgrfis  29386  umgr2wlkon  30006  numclwwlk5  30446  connpconn  35410  cvmliftmolem2  35457  cvmlift2lem10  35487  cvmlift3lem2  35495  cvmlift3lem8  35501  broutsideof3  36301  unblimceq0  36682  paddasslem10  40126  lhpexle2lem  40306  lhpexle3lem  40308  cdlemj3  41120  cdlemkid4  41231  mpaaeu  43428  stoweidlem35  46315  stoweidlem56  46336  stoweidlem59  46339  2arwcat  49881