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

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

Proof of Theorem simp12l
StepHypRef Expression
1 simp2l 1193 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant1 1127 1 (((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  ackbij1lem16  9651  axcontlem4  26686  eqlkr  36121  athgt  36478  llncvrlpln2  36579  4atlem11b  36630  2lnat  36806  cdlemblem  36815  pclfinN  36922  lhp2lt  37023  lhpmcvr5N  37049  lhpmcvr6N  37050  lhp2at0  37054  lhp2atnle  37055  lhp2at0nle  37057  4atexlemex6  37096  cdlemd2  37221  cdlemd7  37226  cdlemd8  37227  cdlemd9  37228  cdleme7aa  37264  cdleme7c  37267  cdleme7d  37268  cdleme7e  37269  cdleme7ga  37270  cdleme7  37271  cdleme11c  37283  cdleme11dN  37284  cdleme11e  37285  cdleme11  37292  cdleme14  37295  cdleme15a  37296  cdleme15b  37297  cdleme15d  37299  cdleme15  37300  cdleme16b  37301  cdleme16c  37302  cdleme16d  37303  cdleme18d  37317  cdleme19b  37326  cdleme19e  37329  cdleme20d  37334  cdleme20g  37337  cdleme20h  37338  cdleme20i  37339  cdleme20j  37340  cdleme20l2  37343  cdleme20l  37344  cdleme20m  37345  cdleme21c  37349  cdleme21ct  37351  cdleme21d  37352  cdleme21e  37353  cdleme22cN  37364  cdleme22f  37368  cdleme22f2  37369  cdleme23a  37371  cdleme23b  37372  cdleme23c  37373  cdleme25a  37375  cdleme25dN  37378  cdleme26fALTN  37384  cdleme26f  37385  cdleme26f2ALTN  37386  cdleme26f2  37387  cdlemefr29bpre0N  37428  cdlemefr29clN  37429  cdlemefr32fvaN  37431  cdlemefr32fva1  37432  cdleme41sn3a  37455  cdleme32le  37469  cdleme35a  37470  cdleme35fnpq  37471  cdleme35b  37472  cdleme35c  37473  cdleme35d  37474  cdleme35e  37475  cdleme35f  37476  cdleme36a  37482  cdleme37m  37484  cdleme39n  37488  cdleme43bN  37512  cdleme43dN  37514  cdleme17d2  37517  cdlemeg46c  37535  cdlemeg46nlpq  37539  cdlemeg46ngfr  37540  cdlemeg46req  37551  cdlemeg46gfv  37552  cdleme50trn1  37571  cdleme50trn2a  37572  cdlemf1  37583  trlord  37591  cdlemb3  37628  cdlemg7fvbwN  37629  cdlemg7aN  37647  cdlemg10a  37662  cdlemg10  37663  cdlemg12d  37668  cdlemg12e  37669  cdlemg12f  37670  cdlemg12g  37671  cdlemg12  37672  cdlemg13a  37673  cdlemg13  37674  cdlemg17b  37684  cdlemg17f  37688  cdlemg17g  37689  cdlemg17h  37690  cdlemg17pq  37694  cdlemg17  37699  cdlemg19a  37705  cdlemg19  37706  cdlemg21  37708  cdlemg27a  37714  cdlemg27b  37718  cdlemg31c  37721  cdlemg33b0  37723  cdlemg33a  37728  trlcone  37750  cdlemg44  37755  cdlemg48  37759  cdlemk37  37936  cdlemky  37948  cdlemk11ta  37951  cdleml4N  38001  dihord1  38240  dihord2pre2  38248  dihord4  38280  dihord5apre  38284  dihmeetlem1N  38312  dihglblem3N  38317  dihglbcpreN  38322  dihmeetlem3N  38327  dihmeetlem13N  38341  mapdpglem32  38727  baerlem3lem2  38732  baerlem5alem2  38733  baerlem5blem2  38734  mzpcong  39453
  Copyright terms: Public domain W3C validator