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

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

Proof of Theorem simp2rl
StepHypRef Expression
1 simprl 778 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant2 1157 1 ((𝜃 ∧ (𝜒 ∧ (𝜑𝜓)) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  tfrlem5  7712  omeu  7902  wemaplem3  8692  gruina  9925  4sqlem18  15883  vdwlem10  15911  mdetuni0  20638  mdetmul  20640  tsmsxp  22171  ax5seglem3  26025  btwnconn1lem1  32515  btwnconn1lem2  32516  btwnconn1lem3  32517  btwnconn1lem4  32518  btwnconn1lem12  32526  btwnconn1lem13  32527  linethru  32581  2llnjN  35347  2lplnja  35399  2lplnj  35400  cdlemblem  35573  dalaw  35666  pclfinN  35680  lhpmcvr4N  35806  lhp2atne  35814  lhp2at0ne  35816  cdlemb2  35821  cdlemd7  35985  cdleme01N  36002  cdleme02N  36003  cdleme0ex2N  36005  cdleme7aa  36023  cdleme7c  36026  cdleme7d  36027  cdleme7e  36028  cdleme7ga  36029  cdleme11a  36041  cdleme20k  36100  cdleme21d  36111  cdleme27cl  36147  cdlemefrs29bpre0  36177  cdlemefrs29cpre1  36179  cdlemefrs32fva  36181  cdlemefrs32fva1  36182  cdlemefr29exN  36183  cdlemefr32sn2aw  36185  cdlemefr31fv1  36192  cdlemefs32sn1aw  36195  cdlemefr44  36206  cdlemefr45e  36209  cdleme41sn3a  36214  cdleme35a  36229  cdleme35fnpq  36230  cdleme35b  36231  cdleme35c  36232  cdleme35d  36233  cdleme35e  36234  cdleme35f  36235  cdleme35sn3a  36240  cdleme42e  36260  cdleme42h  36263  cdleme42i  36264  cdleme17d2  36276  cdleme48fv  36280  cdleme48bw  36283  cdleme48b  36284  cdlemeg46c  36294  cdlemeg46ngfr  36299  cdleme48d  36316  cdlemg2kq  36383  cdlemg2m  36385  cdlemg7fvN  36405  cdlemg8a  36408  cdlemg11aq  36419  cdlemg10c  36420  cdlemg17a  36442  cdlemg31b0N  36475  cdlemg41  36499  cdlemh2  36597  cdlemi  36601  cdlemk21-2N  36672  dihmeetlem1N  37071  dihmeetlem13N  37100  expmordi  38013  iunrelexpmin1  38500
  Copyright terms: Public domain W3C validator