Theorem simprr1 1219

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  poxp2  8131  sqrmo  15202  icodiamlt  15386  psgnunilem2  19404  haust1  23076  cnhaus  23078  isreg2  23101  llynlly  23201  restnlly  23206  llyrest  23209  llyidm  23212  nllyidm  23213  cldllycmp  23219  txlly  23360  txnlly  23361  pthaus  23362  txhaus  23371  txkgen  23376  xkohaus  23377  xkococnlem  23383  hauspwpwf1  23711  itg2add  25509  ulmdvlem3  26150  nosupno  27442  noinfno  27457  etasslt  27551  scutbdaybnd  27553  scutbdaybnd2  27554  addsproplem6  27696  negsproplem6  27746  mulsproplem13  27823  mulsproplem14  27824  mulsprop  27825  ax5seglem6  28459  fusgrfis  28854  umgr2wlkon  29471  numclwwlk5  29908  connpconn  34524  cvmliftmolem2  34571  cvmlift2lem10  34601  cvmlift3lem2  34609  cvmlift3lem8  34615  broutsideof3  35402  unblimceq0  35686  paddasslem10  39003  lhpexle2lem  39183  lhpexle3lem  39185  cdlemj3  39997  cdlemkid4  40108  mpaaeu  42194  stoweidlem35  45049  stoweidlem56  45070  stoweidlem59  45073