MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprr2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 simp2 1138 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antll 728 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  poxp2  8080  icodiamlt  15327  psgnunilem2  19284  haust1  22719  cnhaus  22721  isreg2  22744  llynlly  22844  restnlly  22849  llyrest  22852  llyidm  22855  nllyidm  22856  cldllycmp  22862  txlly  23003  txnlly  23004  pthaus  23005  txhaus  23014  txkgen  23019  xkohaus  23020  xkococnlem  23026  cmetcaulem  24668  itg2add  25140  ulmdvlem3  25777  nosupprefixmo  27064  noinfprefixmo  27065  etasslt  27174  scutbdaybnd  27176  scutbdaybnd2  27177  addsproplem6  27308  negsproplem6  27353  ax5seglem6  27925  n4cyclfrgr  29277  connpconn  33869  cvmlift3lem2  33954  cvmlift3lem8  33960  broutsideof3  34740  unblimceq0  34999  paddasslem10  38321  lhpexle2lem  38501  lhpexle3lem  38503  stoweidlem35  44350  stoweidlem56  44371  stoweidlem59  44374
  Copyright terms: Public domain W3C validator