Theorem simprr2 1221

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 1136	. 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:  icodiamlt  15147  psgnunilem2  19103  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  n4cyclfrgr  28655  connpconn  33197  cvmlift3lem2  33282  cvmlift3lem8  33288  poxp2  33790  poxp3  33796  nosupprefixmo  33903  noinfprefixmo  33904  etasslt  34007  scutbdaybnd  34009  scutbdaybnd2  34010  broutsideof3  34428  unblimceq0  34687  paddasslem10  37843  lhpexle2lem  38023  lhpexle3lem  38025  stoweidlem35  43576  stoweidlem56  43597  stoweidlem59  43600