Theorem simprr2 1223

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

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

This theorem is referenced by:  poxp2  8147  icodiamlt  15459  psgnunilem2  19481  haust1  23295  cnhaus  23297  isreg2  23320  llynlly  23420  restnlly  23425  llyrest  23428  llyidm  23431  nllyidm  23432  cldllycmp  23438  txlly  23579  txnlly  23580  pthaus  23581  txhaus  23590  txkgen  23595  xkohaus  23596  xkococnlem  23602  cmetcaulem  25245  itg2add  25717  ulmdvlem3  26368  nosupprefixmo  27669  noinfprefixmo  27670  etasslt  27782  scutbdaybnd  27784  scutbdaybnd2  27785  addsproplem6  27938  negsproplem6  27996  mulsproplem13  28088  mulsproplem14  28089  mulsprop  28090  ax5seglem6  28918  n4cyclfrgr  30277  connpconn  35262  cvmlift3lem2  35347  cvmlift3lem8  35353  broutsideof3  36149  unblimceq0  36530  paddasslem10  39853  lhpexle2lem  40033  lhpexle3lem  40035  stoweidlem35  46031  stoweidlem56  46052  stoweidlem59  46055  2arwcat  49444