Theorem simprr3 1225

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 1139	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antll 730	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  7989  poxp2  8093  ttrcltr  9637  icodiamlt  15400  psgnunilem2  19470  srgbinom  20212  psgndiflemA  21581  haust1  23317  cnhaus  23319  isreg2  23342  llynlly  23442  restnlly  23447  llyrest  23450  llyidm  23453  nllyidm  23454  cldllycmp  23460  txlly  23601  txnlly  23602  pthaus  23603  txhaus  23612  txkgen  23617  xkohaus  23618  xkococnlem  23624  cmetcaulem  25255  itg2add  25726  ulmdvlem3  26367  nosupprefixmo  27664  noinfprefixmo  27665  nosupno  27667  noinfno  27682  etaslts  27785  cutbdaybnd  27787  cutbdaybnd2  27788  addsproplem6  27966  negsproplem6  28025  mulsproplem13  28120  mulsproplem14  28121  mulsprop  28122  bdayfinbndlem1  28459  ax5seglem6  29003  fusgrfis  29399  wwlksnextfun  29966  umgr2wlkon  30018  connpconn  35417  cvmlift3lem2  35502  cvmlift3lem8  35508  ifscgr  36226  broutsideof3  36308  unblimceq0  36767  paddasslem10  40275  lhpexle2lem  40455  lhpexle3lem  40457  mpaaeu  43578  stoweidlem35  46463  stoweidlem56  46484  stoweidlem59  46487  2arwcat  50069