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

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

Proof of Theorem simp11r
StepHypRef Expression
1 simp1r 1241 . 2 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜓)
213ad2ant1 1128 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:  pceu  15753  maduf  20649  nllyrest  21491  exatleN  35193  2llnjaN  35355  2lplnja  35408  dalemceb  35427  pclfinN  35689  lhpexle3lem  35800  lhpmcvr5N  35816  lhpmcvr6N  35817  lhp2at0  35821  4atexlemw  35837  cdlemd2  35989  cdlemd4  35991  cdleme7aa  36032  cdleme7c  36035  cdleme7d  36036  cdleme7e  36037  cdleme7ga  36038  cdleme7  36039  cdleme15a  36064  cdleme15b  36065  cdleme15d  36067  cdleme15  36068  cdleme16b  36069  cdleme16c  36070  cdleme16d  36071  cdleme16e  36072  cdleme16f  36073  cdleme18d  36085  cdleme19b  36094  cdleme19d  36096  cdleme19e  36097  cdleme20d  36102  cdleme20e  36103  cdleme20f  36104  cdleme20g  36105  cdleme20h  36106  cdleme20j  36108  cdleme20k  36109  cdleme20l1  36110  cdleme20l2  36111  cdleme20l  36112  cdleme20m  36113  cdleme21c  36117  cdleme21ct  36119  cdleme22cN  36132  cdleme22f  36136  cdleme22g  36138  cdleme23a  36139  cdleme23b  36140  cdleme23c  36141  cdleme25a  36143  cdleme25c  36145  cdleme25dN  36146  cdleme26ee  36150  cdleme26eALTN  36151  cdleme27N  36159  cdleme28a  36160  cdleme28b  36161  cdleme29ex  36164  cdlemefr29exN  36192  cdleme32b  36232  cdleme32c  36233  cdleme32e  36235  cdleme35b  36240  cdleme35c  36241  cdleme35d  36242  cdleme35e  36243  cdleme35f  36244  cdleme42h  36272  cdleme42i  36273  cdleme42k  36274  cdleme48bw  36292  cdlemeg46frv  36315  cdlemeg46vrg  36317  cdlemeg46rgv  36318  cdlemeg46req  36319  cdlemf1  36351  trlord  36359  cdlemg7fvbwN  36397  cdlemg10  36431  cdlemg12e  36437  cdlemg12f  36438  cdlemg19a  36473  cdlemg31c  36489  cdlemg33c0  36492  cdlemg35  36503  tendococl  36562  cdlemh2  36606  cdlemh  36607  cdlemi  36610  cdlemk5  36626  cdlemk7  36638  cdlemk11  36639  cdlemk5u  36651  cdlemkj  36653  cdlemkuv2  36657  cdlemk7u  36660  cdlemk11u  36661  cdlemk26-3  36696  cdlemk11t  36736  cdlemk52  36744  cdlemk53a  36745  dihord1  37009  dihord2a  37010  dihord2b  37011  dihord11b  37013  dihord11c  37015  dihord2pre  37016  dihord2pre2  37017  dihord5apre  37053  dihmeetlem1N  37081  dihglblem2N  37085  dihglblem3N  37086  dihglbcpreN  37091  dihmeetlem3N  37096  dihjatc1  37102  suplesup  40053  limsupre  40376  sge0xaddlem2  41154
  Copyright terms: Public domain W3C validator