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

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

Proof of Theorem simp22l
StepHypRef Expression
1 simp2l 1085 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant2 1081 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  ax5seglem6  25714  segconeu  31760  3atlem2  34250  lplncvrlvol2  34381  paddasslem15  34600  4atex  34842  trlval4  34955  cdlemc5  34962  cdlemc6  34963  cdlemd2  34966  cdlemd3  34967  cdlemd4  34968  cdleme0moN  34992  cdleme3g  35001  cdleme3h  35002  cdleme3  35004  cdleme11g  35032  cdleme11h  35033  cdleme11j  35034  cdleme11k  35035  cdleme11l  35036  cdleme11  35037  cdleme14  35040  cdleme15a  35041  cdleme15c  35043  cdleme15d  35044  cdleme15  35045  cdleme16b  35046  cdleme16c  35047  cdleme16d  35048  cdleme16e  35049  cdleme16f  35050  cdleme18a  35058  cdleme18b  35059  cdleme18c  35060  cdleme19b  35072  cdleme19e  35075  cdleme20bN  35078  cdleme20c  35079  cdleme20d  35080  cdleme20e  35081  cdleme20f  35082  cdleme20g  35083  cdleme20h  35084  cdleme20j  35086  cdleme20l2  35089  cdleme20l  35090  cdleme20m  35091  cdleme21ct  35097  cdleme22d  35111  cdleme22e  35112  cdleme22eALTN  35113  cdleme26e  35127  cdleme27a  35135  cdleme28a  35138  cdleme30a  35146  cdleme43fsv1snlem  35188  cdlemefs44  35194  cdlemefs45ee  35198  cdleme35sn2aw  35226  cdleme36a  35228  cdleme39n  35234  cdleme40m  35235  cdleme42k  35252  cdlemeg47rv2  35278  cdlemeg46frv  35293  cdlemeg46vrg  35295  cdlemeg46rgv  35296  cdlemeg46req  35297  cdlemg2fv2  35368  cdlemg4g  35384  cdlemg4  35385  cdlemg6c  35388  cdlemg8b  35396  cdlemg8c  35397  cdlemg9a  35400  cdlemg9b  35401  cdlemg9  35402  cdlemg12a  35411  cdlemg12b  35412  cdlemg12c  35413  cdlemg17h  35436  cdlemg18b  35447  cdlemg18c  35448  cdlemg31b0a  35463  cdlemg27b  35464  cdlemg31d  35468  cdlemg28b  35471  cdlemg33a  35474  cdlemg33b  35475  cdlemg33c  35476  cdlemg33d  35477  cdlemg33e  35478  cdlemg33  35479  cdlemh  35585  cdlemk6  35605  cdlemki  35609  cdlemksat  35614  cdlemksv2  35615  cdlemk7  35616  cdlemk11  35617  cdlemk12  35618  cdlemkole  35621  cdlemk14  35622  cdlemk15  35623  cdlemk17  35626  cdlemk1u  35627  cdlemk5u  35629  cdlemk6u  35630  cdlemk7u  35638  cdlemk11u  35639  cdlemk12u  35640  cdlemk7u-2N  35656  cdlemk11u-2N  35657  cdlemk12u-2N  35658  cdlemk20-2N  35660  cdlemk28-3  35676  cdlemk33N  35677  cdlemk34  35678  cdlemk37  35682  cdlemk39  35684  cdlemk35s  35705  cdlemk39s  35707  cdlemk47  35717  cdlemk48  35718  cdlemk50  35720  cdlemk51  35721  cdlemk52  35722  cdlemkyyN  35730  cdlemk43N  35731  cdlemn2  35964  cdlemn10  35975
  Copyright terms: Public domain W3C validator