Theorem simprr2 1224

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simprr2	⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)

Proof of Theorem simprr2

Step	Hyp	Ref	Expression
1		simp2 1138	. 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:  poxp2  8084  icodiamlt  15389  psgnunilem2  19459  haust1  23326  cnhaus  23328  isreg2  23351  llynlly  23451  restnlly  23456  llyrest  23459  llyidm  23462  nllyidm  23463  cldllycmp  23469  txlly  23610  txnlly  23611  pthaus  23612  txhaus  23621  txkgen  23626  xkohaus  23627  xkococnlem  23633  cmetcaulem  25264  itg2add  25735  ulmdvlem3  26382  nosupprefixmo  27683  noinfprefixmo  27684  etaslts  27804  cutbdaybnd  27806  cutbdaybnd2  27807  addsproplem6  27985  negsproplem6  28044  mulsproplem13  28139  mulsproplem14  28140  mulsprop  28141  bdayfinbndlem1  28478  ax5seglem6  29022  n4cyclfrgr  30381  connpconn  35438  cvmlift3lem2  35523  cvmlift3lem8  35529  broutsideof3  36329  unblimceq0  36780  paddasslem10  40286  lhpexle2lem  40466  lhpexle3lem  40468  stoweidlem35  46478  stoweidlem56  46499  stoweidlem59  46502  pgn4cyclex  48599  2arwcat  50072