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

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

Proof of Theorem simp2rl
StepHypRef Expression
1 simprl 811 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant2 1126 1 ((𝜃 ∧ (𝜒 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  tfrlem5  7633  omeu  7822  wemaplem3  8606  gruina  9803  4sqlem18  15839  vdwlem10  15867  mdetuni0  20600  mdetmul  20602  tsmsxp  22130  ax5seglem3  25981  btwnconn1lem1  32471  btwnconn1lem2  32472  btwnconn1lem3  32473  btwnconn1lem4  32474  btwnconn1lem12  32482  btwnconn1lem13  32483  linethru  32537  2llnjN  35325  2lplnja  35377  2lplnj  35378  cdlemblem  35551  dalaw  35644  pclfinN  35658  lhpmcvr4N  35784  lhp2atne  35792  lhp2at0ne  35794  cdlemb2  35799  cdlemd7  35963  cdleme01N  35980  cdleme02N  35981  cdleme0ex2N  35983  cdleme7aa  36001  cdleme7c  36004  cdleme7d  36005  cdleme7e  36006  cdleme7ga  36007  cdleme11a  36019  cdleme20k  36078  cdleme21d  36089  cdleme27cl  36125  cdlemefrs29bpre0  36155  cdlemefrs29cpre1  36157  cdlemefrs32fva  36159  cdlemefrs32fva1  36160  cdlemefr29exN  36161  cdlemefr32sn2aw  36163  cdlemefr31fv1  36170  cdlemefs32sn1aw  36173  cdlemefr44  36184  cdlemefr45e  36187  cdleme41sn3a  36192  cdleme35a  36207  cdleme35fnpq  36208  cdleme35b  36209  cdleme35c  36210  cdleme35d  36211  cdleme35e  36212  cdleme35f  36213  cdleme35sn3a  36218  cdleme42e  36238  cdleme42h  36241  cdleme42i  36242  cdleme17d2  36254  cdleme48fv  36258  cdleme48bw  36261  cdleme48b  36262  cdlemeg46c  36272  cdlemeg46ngfr  36277  cdleme48d  36294  cdlemg2kq  36361  cdlemg2m  36363  cdlemg7fvN  36383  cdlemg8a  36386  cdlemg11aq  36397  cdlemg10c  36398  cdlemg17a  36420  cdlemg31b0N  36453  cdlemg41  36477  cdlemh2  36575  cdlemi  36579  cdlemk21-2N  36650  dihmeetlem1N  37050  dihmeetlem13N  37079  expmordi  37983  iunrelexpmin1  38471
  Copyright terms: Public domain W3C validator