Theorem simprr3 1223

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  8062  poxp2  8169  ttrcltr  9757  icodiamlt  15475  psgnunilem2  19514  srgbinom  20229  psgndiflemA  21620  haust1  23361  cnhaus  23363  isreg2  23386  llynlly  23486  restnlly  23491  llyrest  23494  llyidm  23497  nllyidm  23498  cldllycmp  23504  txlly  23645  txnlly  23646  pthaus  23647  txhaus  23656  txkgen  23661  xkohaus  23662  xkococnlem  23668  cmetcaulem  25323  itg2add  25795  ulmdvlem3  26446  nosupprefixmo  27746  noinfprefixmo  27747  nosupno  27749  noinfno  27764  etasslt  27859  scutbdaybnd  27861  scutbdaybnd2  27862  addsproplem6  28008  negsproplem6  28066  mulsproplem13  28155  mulsproplem14  28156  mulsprop  28157  ax5seglem6  28950  fusgrfis  29348  wwlksnextfun  29919  umgr2wlkon  29971  connpconn  35241  cvmlift3lem2  35326  cvmlift3lem8  35332  ifscgr  36046  broutsideof3  36128  unblimceq0  36509  paddasslem10  39832  lhpexle2lem  40012  lhpexle3lem  40014  mpaaeu  43167  stoweidlem35  46055  stoweidlem56  46076  stoweidlem59  46079