Theorem simprr1 1240

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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

This theorem is referenced by:  poxp2  8140  sqrmo  15304  icodiamlt  15491  psgnunilem2  19566  haust1  23490  cnhaus  23492  isreg2  23515  llynlly  23615  restnlly  23620  llyrest  23623  llyidm  23626  nllyidm  23627  cldllycmp  23633  txlly  23774  txnlly  23775  pthaus  23776  txhaus  23785  txkgen  23790  xkohaus  23791  xkococnlem  23797  hauspwpwf1  24125  itg2add  25899  ulmdvlem3  26543  nosupno  27845  noinfno  27860  etaslts  27964  cutbdaybnd  27966  cutbdaybnd2  27967  addsproplem6  28145  negsproplem6  28204  mulsproplem13  28299  mulsproplem14  28300  mulsprop  28301  bdayfinbndlem1  28638  ax5seglem6  29262  fusgrfis  29658  umgr2wlkon  30277  numclwwlk5  30717  connpconn  35705  cvmliftmolem2  35752  cvmlift2lem10  35782  cvmlift3lem2  35790  cvmlift3lem8  35796  broutsideof3  36596  unblimceq0  37074  paddasslem10  40581  lhpexle2lem  40761  lhpexle3lem  40763  cdlemj3  41575  cdlemkid4  41686  mpaaeu  43857  stoweidlem35  46729  stoweidlem56  46750  stoweidlem59  46753  2arwcat  50355