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

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

Proof of Theorem simp13l
StepHypRef Expression
1 simp3l 1243 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant1 1127 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  pceu  15758  axpasch  26042  3atlem4  35294  llncvrlpln2  35365  2lplnja  35427  2lnat  35592  llnexchb2  35677  lhp2lt  35809  lhpmcvr5N  35835  4atexlemq  35859  4atexlemex6  35882  trlval2  35972  cdleme7d  36055  cdleme7e  36056  cdleme7ga  36057  cdleme7  36058  cdleme11l  36078  cdleme11  36079  cdleme14  36082  cdleme15a  36083  cdleme15b  36084  cdleme15  36087  cdleme16b  36088  cdleme16c  36089  cdleme16d  36090  cdleme18d  36104  cdleme19b  36113  cdleme19e  36116  cdleme20d  36121  cdleme20g  36124  cdleme20h  36125  cdleme20i  36126  cdleme20j  36127  cdleme20l2  36130  cdleme20l  36131  cdleme20m  36132  cdleme21d  36139  cdleme21e  36140  cdleme21h  36143  cdleme22f  36155  cdleme23a  36158  cdleme23b  36159  cdleme23c  36160  cdleme24  36161  cdleme25a  36162  cdleme25dN  36165  cdleme26ee  36169  cdleme26fALTN  36171  cdleme26f  36172  cdleme26f2ALTN  36173  cdleme26f2  36174  cdleme27a  36176  cdlemefr29bpre0N  36215  cdlemefr29clN  36216  cdlemefr32fvaN  36218  cdlemefr32fva1  36219  cdleme41sn3a  36242  cdleme35a  36257  cdleme35fnpq  36258  cdleme35b  36259  cdleme35c  36260  cdleme35d  36261  cdleme35f  36263  cdleme36m  36270  cdleme37m  36271  cdleme39n  36275  cdleme43bN  36299  cdleme43dN  36301  cdleme17d2  36304  cdlemeg46c  36322  cdlemeg46nlpq  36326  cdlemeg46ngfr  36327  cdlemeg46req  36338  cdlemeg46gfv  36339  cdleme50trn1  36358  cdleme50trn2a  36359  cdlemf1  36370  cdlemf  36372  cdlemg10a  36449  cdlemg10  36450  cdlemg12d  36455  cdlemg12e  36456  cdlemg12f  36457  cdlemg12g  36458  cdlemg12  36459  cdlemg13  36461  cdlemg16ALTN  36467  cdlemg17b  36471  cdlemg17h  36477  cdlemg17pq  36481  cdlemg17iqN  36483  cdlemg17  36486  cdlemg19a  36492  cdlemg19  36493  cdlemg21  36495  cdlemg27a  36501  cdlemg27b  36505  cdlemg31c  36508  cdlemg33b0  36510  cdlemg33a  36515  cdlemg48  36546  tendocan  36633  cdlemk26-3  36715  cdlemk27-3  36716  cdlemk28-3  36717  cdlemk37  36723  cdlemky  36735  cdlemkyu  36736  cdlemk11ta  36738  cdlemkid3N  36742  cdlemk42  36750  cdlemk42yN  36753  cdlemk11t  36755  cdlemk45  36756  cdlemk46  36757  cdlemk47  36758  cdlemk51  36762  cdlemk52  36763  cdlemk53a  36764  cdleml4N  36788  dihord2pre2  37036  dihord4  37068  dihord5apre  37072  dihmeetlem1N  37100  dihmeetlem15N  37131  mapdpglem32  37515  mzpcong  38065  mullimc  40366  mullimcf  40373  addlimc  40398
  Copyright terms: Public domain W3C validator