Theorem simprr3 1240

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  el2xptp0  8032  poxp2  8138  ttrcltr  9684  icodiamlt  15489  psgnunilem2  19564  srgbinom  20312  psgndiflemA  21730  haust1  23488  cnhaus  23490  isreg2  23513  llynlly  23613  restnlly  23618  llyrest  23621  llyidm  23624  nllyidm  23625  cldllycmp  23631  txlly  23772  txnlly  23773  pthaus  23774  txhaus  23783  txkgen  23788  xkohaus  23789  xkococnlem  23795  cmetcaulem  25426  itg2add  25897  ulmdvlem3  26541  nosupprefixmo  27840  noinfprefixmo  27841  nosupno  27843  noinfno  27858  etaslts  27962  cutbdaybnd  27964  cutbdaybnd2  27965  addsproplem6  28143  negsproplem6  28202  mulsproplem13  28297  mulsproplem14  28298  mulsprop  28299  bdayfinbndlem1  28636  ax5seglem6  29250  fusgrfis  29646  wwlksnextfun  30213  umgr2wlkon  30265  connpconn  35693  cvmlift3lem2  35778  cvmlift3lem8  35784  ifscgr  36502  broutsideof3  36584  unblimceq0  37062  paddasslem10  40571  lhpexle2lem  40751  lhpexle3lem  40753  mpaaeu  43847  stoweidlem35  46719  stoweidlem56  46740  stoweidlem59  46743  2arwcat  50345