Theorem simprr3 1222

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  el2xptp0  7878  ttrcltr  9474  icodiamlt  15147  psgnunilem2  19103  srgbinom  19781  psgndiflemA  20806  haust1  22503  cnhaus  22505  isreg2  22528  llynlly  22628  restnlly  22633  llyrest  22636  llyidm  22639  nllyidm  22640  cldllycmp  22646  txlly  22787  txnlly  22788  pthaus  22789  txhaus  22798  txkgen  22803  xkohaus  22804  xkococnlem  22810  cmetcaulem  24452  itg2add  24924  ulmdvlem3  25561  ax5seglem6  27302  fusgrfis  27697  wwlksnextfun  28263  umgr2wlkon  28315  connpconn  33197  cvmlift3lem2  33282  cvmlift3lem8  33288  poxp2  33790  nosupprefixmo  33903  noinfprefixmo  33904  nosupno  33906  noinfno  33921  etasslt  34007  scutbdaybnd  34009  scutbdaybnd2  34010  ifscgr  34346  broutsideof3  34428  unblimceq0  34687  paddasslem10  37843  lhpexle2lem  38023  lhpexle3lem  38025  mpaaeu  40975  stoweidlem35  43576  stoweidlem56  43597  stoweidlem59  43600