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

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

Proof of Theorem simp13l
StepHypRef Expression
1 simp3l 1197 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant1 1129 1 (((𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜏𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  pceu  16182  axpasch  26726  3atlem4  36621  llncvrlpln2  36692  2lplnja  36754  2lnat  36919  llnexchb2  37004  lhp2lt  37136  lhpmcvr5N  37162  4atexlemq  37186  4atexlemex6  37209  trlval2  37298  cdleme7d  37381  cdleme7e  37382  cdleme7ga  37383  cdleme7  37384  cdleme11l  37404  cdleme11  37405  cdleme14  37408  cdleme15a  37409  cdleme15b  37410  cdleme15  37413  cdleme16b  37414  cdleme16c  37415  cdleme16d  37416  cdleme18d  37430  cdleme19b  37439  cdleme19e  37442  cdleme20d  37447  cdleme20g  37450  cdleme20h  37451  cdleme20i  37452  cdleme20j  37453  cdleme20l2  37456  cdleme20l  37457  cdleme20m  37458  cdleme21d  37465  cdleme21e  37466  cdleme21h  37469  cdleme22f  37481  cdleme23a  37484  cdleme23b  37485  cdleme23c  37486  cdleme24  37487  cdleme25a  37488  cdleme25dN  37491  cdleme26ee  37495  cdleme26fALTN  37497  cdleme26f  37498  cdleme26f2ALTN  37499  cdleme26f2  37500  cdleme27a  37502  cdlemefr29bpre0N  37541  cdlemefr29clN  37542  cdlemefr32fvaN  37544  cdlemefr32fva1  37545  cdleme41sn3a  37568  cdleme35a  37583  cdleme35fnpq  37584  cdleme35b  37585  cdleme35c  37586  cdleme35d  37587  cdleme35f  37589  cdleme36m  37596  cdleme37m  37597  cdleme39n  37601  cdleme43bN  37625  cdleme43dN  37627  cdleme17d2  37630  cdlemeg46c  37648  cdlemeg46nlpq  37652  cdlemeg46ngfr  37653  cdlemeg46req  37664  cdlemeg46gfv  37665  cdleme50trn1  37684  cdleme50trn2a  37685  cdlemf1  37696  cdlemf  37698  cdlemg10a  37775  cdlemg10  37776  cdlemg12d  37781  cdlemg12e  37782  cdlemg12f  37783  cdlemg12g  37784  cdlemg12  37785  cdlemg13  37787  cdlemg16ALTN  37793  cdlemg17b  37797  cdlemg17h  37803  cdlemg17pq  37807  cdlemg17iqN  37809  cdlemg17  37812  cdlemg19a  37818  cdlemg19  37819  cdlemg21  37821  cdlemg27a  37827  cdlemg27b  37831  cdlemg31c  37834  cdlemg33b0  37836  cdlemg33a  37841  cdlemg48  37872  tendocan  37959  cdlemk26-3  38041  cdlemk27-3  38042  cdlemk28-3  38043  cdlemk37  38049  cdlemky  38061  cdlemkyu  38062  cdlemk11ta  38064  cdlemkid3N  38068  cdlemk42  38076  cdlemk42yN  38079  cdlemk11t  38081  cdlemk45  38082  cdlemk46  38083  cdlemk47  38084  cdlemk51  38088  cdlemk52  38089  cdlemk53a  38090  cdleml4N  38114  dihord2pre2  38361  dihord4  38393  dihord5apre  38397  dihmeetlem1N  38425  dihmeetlem15N  38456  mapdpglem32  38840  mzpcong  39567  mullimc  41895  mullimcf  41902  addlimc  41927
  Copyright terms: Public domain W3C validator