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

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

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 1089

This theorem is referenced by:  el2xptp0  8077  poxp2  8184  ttrcltr  9785  icodiamlt  15484  psgnunilem2  19537  srgbinom  20258  psgndiflemA  21642  haust1  23381  cnhaus  23383  isreg2  23406  llynlly  23506  restnlly  23511  llyrest  23514  llyidm  23517  nllyidm  23518  cldllycmp  23524  txlly  23665  txnlly  23666  pthaus  23667  txhaus  23676  txkgen  23681  xkohaus  23682  xkococnlem  23688  cmetcaulem  25341  itg2add  25814  ulmdvlem3  26463  nosupprefixmo  27763  noinfprefixmo  27764  nosupno  27766  noinfno  27781  etasslt  27876  scutbdaybnd  27878  scutbdaybnd2  27879  addsproplem6  28025  negsproplem6  28083  mulsproplem13  28172  mulsproplem14  28173  mulsprop  28174  ax5seglem6  28967  fusgrfis  29365  wwlksnextfun  29931  umgr2wlkon  29983  connpconn  35203  cvmlift3lem2  35288  cvmlift3lem8  35294  ifscgr  36008  broutsideof3  36090  unblimceq0  36473  paddasslem10  39786  lhpexle2lem  39966  lhpexle3lem  39968  mpaaeu  43107  stoweidlem35  45956  stoweidlem56  45977  stoweidlem59  45980