Theorem simprr3 1224

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simprr3	⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

Proof of Theorem simprr3

Step	Hyp	Ref	Expression
1		simp3 1138	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antll 729	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  el2xptp0  8018  poxp2  8125  ttrcltr  9676  icodiamlt  15411  psgnunilem2  19432  srgbinom  20147  psgndiflemA  21517  haust1  23246  cnhaus  23248  isreg2  23271  llynlly  23371  restnlly  23376  llyrest  23379  llyidm  23382  nllyidm  23383  cldllycmp  23389  txlly  23530  txnlly  23531  pthaus  23532  txhaus  23541  txkgen  23546  xkohaus  23547  xkococnlem  23553  cmetcaulem  25195  itg2add  25667  ulmdvlem3  26318  nosupprefixmo  27619  noinfprefixmo  27620  nosupno  27622  noinfno  27637  etasslt  27732  scutbdaybnd  27734  scutbdaybnd2  27735  addsproplem6  27888  negsproplem6  27946  mulsproplem13  28038  mulsproplem14  28039  mulsprop  28040  ax5seglem6  28868  fusgrfis  29264  wwlksnextfun  29835  umgr2wlkon  29887  connpconn  35229  cvmlift3lem2  35314  cvmlift3lem8  35320  ifscgr  36039  broutsideof3  36121  unblimceq0  36502  paddasslem10  39830  lhpexle2lem  40010  lhpexle3lem  40012  mpaaeu  43146  stoweidlem35  46040  stoweidlem56  46061  stoweidlem59  46064  2arwcat  49593