Theorem simprr2 1235

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  poxp2  8118  icodiamlt  15448  psgnunilem2  19518  haust1  23392  cnhaus  23394  isreg2  23417  llynlly  23517  restnlly  23522  llyrest  23525  llyidm  23528  nllyidm  23529  cldllycmp  23535  txlly  23676  txnlly  23677  pthaus  23678  txhaus  23687  txkgen  23692  xkohaus  23693  xkococnlem  23699  cmetcaulem  25330  itg2add  25801  ulmdvlem3  26442  nosupprefixmo  27741  noinfprefixmo  27742  etaslts  27863  cutbdaybnd  27865  cutbdaybnd2  27866  addsproplem6  28044  negsproplem6  28103  mulsproplem13  28198  mulsproplem14  28199  mulsprop  28200  bdayfinbndlem1  28537  ax5seglem6  29081  n4cyclfrgr  30439  connpconn  35549  cvmlift3lem2  35634  cvmlift3lem8  35640  broutsideof3  36440  unblimceq0  36909  paddasslem10  40417  lhpexle2lem  40597  lhpexle3lem  40599  stoweidlem35  46573  stoweidlem56  46594  stoweidlem59  46597  pgn4cyclex  48712  2arwcat  50185