Theorem simprr2 1222

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 727	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  poxp2  8128  icodiamlt  15381  psgnunilem2  19362  haust1  22855  cnhaus  22857  isreg2  22880  llynlly  22980  restnlly  22985  llyrest  22988  llyidm  22991  nllyidm  22992  cldllycmp  22998  txlly  23139  txnlly  23140  pthaus  23141  txhaus  23150  txkgen  23155  xkohaus  23156  xkococnlem  23162  cmetcaulem  24804  itg2add  25276  ulmdvlem3  25913  nosupprefixmo  27200  noinfprefixmo  27201  etasslt  27311  scutbdaybnd  27313  scutbdaybnd2  27314  addsproplem6  27455  negsproplem6  27504  mulsproplem13  27581  mulsproplem14  27582  mulsprop  27583  ax5seglem6  28189  n4cyclfrgr  29541  connpconn  34221  cvmlift3lem2  34306  cvmlift3lem8  34312  broutsideof3  35093  unblimceq0  35378  paddasslem10  38695  lhpexle2lem  38875  lhpexle3lem  38877  stoweidlem35  44741  stoweidlem56  44762  stoweidlem59  44765