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

Theorem simprr1 1107
 Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simprr1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜑)

Proof of Theorem simprr1
StepHypRef Expression
1 simpr1 1065 . 2 ((𝜃 ∧ (𝜑𝜓𝜒)) → 𝜑)
21adantl 482 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036 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 197  df-an 386  df-3an 1038 This theorem is referenced by:  sqrmo  13921  icodiamlt  14103  psgnunilem2  17831  haust1  21061  cnhaus  21063  isreg2  21086  llynlly  21185  restnlly  21190  llyrest  21193  llyidm  21196  nllyidm  21197  cldllycmp  21203  txlly  21344  txnlly  21345  pthaus  21346  txhaus  21355  txkgen  21360  xkohaus  21361  xkococnlem  21367  hauspwpwf1  21696  itg2add  23427  ulmdvlem3  24055  ax5seglem6  25709  fusgrfis  26104  umgr2wlkon  26709  numclwlk1lem2f  27074  numclwwlk5  27094  connpconn  30917  cvmliftmolem2  30964  cvmlift2lem10  30994  cvmlift3lem2  31002  cvmlift3lem8  31008  broutsideof3  31848  unblimceq0  32113  paddasslem10  34562  lhpexle2lem  34742  lhpexle3lem  34744  cdlemj3  35558  cdlemkid4  35669  mpaaeu  37168  stoweidlem35  39527  stoweidlem56  39548  stoweidlem59  39551
 Copyright terms: Public domain W3C validator