Theorem simprr1 1228

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp2  8090  sqrmo  15211  icodiamlt  15398  psgnunilem2  19468  haust1  23342  cnhaus  23344  isreg2  23367  llynlly  23467  restnlly  23472  llyrest  23475  llyidm  23478  nllyidm  23479  cldllycmp  23485  txlly  23626  txnlly  23627  pthaus  23628  txhaus  23637  txkgen  23642  xkohaus  23643  xkococnlem  23649  hauspwpwf1  23977  itg2add  25751  ulmdvlem3  26392  nosupno  27692  noinfno  27707  etaslts  27810  cutbdaybnd  27812  cutbdaybnd2  27813  addsproplem6  27991  negsproplem6  28050  mulsproplem13  28145  mulsproplem14  28146  mulsprop  28147  bdayfinbndlem1  28484  ax5seglem6  29028  fusgrfis  29424  umgr2wlkon  30043  numclwwlk5  30483  connpconn  35470  cvmliftmolem2  35517  cvmlift2lem10  35547  cvmlift3lem2  35555  cvmlift3lem8  35561  broutsideof3  36361  unblimceq0  36820  paddasslem10  40328  lhpexle2lem  40508  lhpexle3lem  40510  cdlemj3  41322  cdlemkid4  41433  mpaaeu  43602  stoweidlem35  46485  stoweidlem56  46506  stoweidlem59  46509  2arwcat  50097