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 742	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8148  sqrmo  15328  icodiamlt  15515  psgnunilem2  19596  haust1  23546  cnhaus  23548  isreg2  23571  llynlly  23671  restnlly  23676  llyrest  23679  llyidm  23682  nllyidm  23683  cldllycmp  23689  txlly  23830  txnlly  23831  pthaus  23832  txhaus  23841  txkgen  23846  xkohaus  23847  xkococnlem  23853  hauspwpwf1  24181  itg2add  25955  ulmdvlem3  26602  nosupno  27904  noinfno  27919  etaslts  28023  cutbdaybnd  28025  cutbdaybnd2  28026  addsproplem6  28204  negsproplem6  28263  mulsproplem13  28358  mulsproplem14  28359  mulsprop  28360  bdayfinbndlem1  28697  ax5seglem6  29321  fusgrfis  29717  umgr2wlkon  30336  numclwwlk5  30776  connpconn  35748  cvmliftmolem2  35795  cvmlift2lem10  35825  cvmlift3lem2  35833  cvmlift3lem8  35839  broutsideof3  36639  unblimceq0  37137  paddasslem10  40644  lhpexle2lem  40824  lhpexle3lem  40826  cdlemj3  41638  cdlemkid4  41749  mpaaeu  43918  stoweidlem35  46790  stoweidlem56  46811  stoweidlem59  46814  2arwcat  50419