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 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antll 729	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  8168  sqrmo  15290  icodiamlt  15474  psgnunilem2  19513  haust1  23360  cnhaus  23362  isreg2  23385  llynlly  23485  restnlly  23490  llyrest  23493  llyidm  23496  nllyidm  23497  cldllycmp  23503  txlly  23644  txnlly  23645  pthaus  23646  txhaus  23655  txkgen  23660  xkohaus  23661  xkococnlem  23667  hauspwpwf1  23995  itg2add  25794  ulmdvlem3  26445  nosupno  27748  noinfno  27763  etasslt  27858  scutbdaybnd  27860  scutbdaybnd2  27861  addsproplem6  28007  negsproplem6  28065  mulsproplem13  28154  mulsproplem14  28155  mulsprop  28156  ax5seglem6  28949  fusgrfis  29347  umgr2wlkon  29970  numclwwlk5  30407  connpconn  35240  cvmliftmolem2  35287  cvmlift2lem10  35317  cvmlift3lem2  35325  cvmlift3lem8  35331  broutsideof3  36127  unblimceq0  36508  paddasslem10  39831  lhpexle2lem  40011  lhpexle3lem  40013  cdlemj3  40825  cdlemkid4  40936  mpaaeu  43162  stoweidlem35  46050  stoweidlem56  46071  stoweidlem59  46074