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  8125  icodiamlt  15411  psgnunilem2  19432  haust1  23246  cnhaus  23248  isreg2  23271  llynlly  23371  restnlly  23376  llyrest  23379  llyidm  23382  nllyidm  23383  cldllycmp  23389  txlly  23530  txnlly  23531  pthaus  23532  txhaus  23541  txkgen  23546  xkohaus  23547  xkococnlem  23553  cmetcaulem  25195  itg2add  25667  ulmdvlem3  26318  nosupprefixmo  27619  noinfprefixmo  27620  etasslt  27732  scutbdaybnd  27734  scutbdaybnd2  27735  addsproplem6  27888  negsproplem6  27946  mulsproplem13  28038  mulsproplem14  28039  mulsprop  28040  ax5seglem6  28868  n4cyclfrgr  30227  connpconn  35229  cvmlift3lem2  35314  cvmlift3lem8  35320  broutsideof3  36121  unblimceq0  36502  paddasslem10  39830  lhpexle2lem  40010  lhpexle3lem  40012  stoweidlem35  46040  stoweidlem56  46061  stoweidlem59  46064  pgn4cyclex  48120  2arwcat  49593