Theorem simprr3 1203

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  el2xptp0  7545  icodiamlt  14650  psgnunilem2  18379  srgbinom  19012  psgndiflemA  20441  haust1  21658  cnhaus  21660  isreg2  21683  llynlly  21783  restnlly  21788  llyrest  21791  llyidm  21794  nllyidm  21795  cldllycmp  21801  txlly  21942  txnlly  21943  pthaus  21944  txhaus  21953  txkgen  21958  xkohaus  21959  xkococnlem  21965  cmetcaulem  23588  itg2add  24057  ulmdvlem3  24687  ax5seglem6  26417  fusgrfis  26809  wwlksnextfun  27383  wwlksnextfunOLD  27388  umgr2wlkon  27450  connpconn  32057  cvmlift3lem2  32142  cvmlift3lem8  32148  noprefixmo  32693  nosupno  32694  scutbdaybnd  32766  ifscgr  32996  broutsideof3  33078  unblimceq0  33336  paddasslem10  36388  lhpexle2lem  36568  lhpexle3lem  36570  mpaaeu  39124  stoweidlem35  41730  stoweidlem56  41751  stoweidlem59  41754