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

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

Proof of Theorem simp22l
StepHypRef Expression
1 simp2l 1191 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant2 1126 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 1081
This theorem is referenced by:  ax5seglem6  26648  segconeu  33370  3atlem2  36502  lplncvrlvol2  36633  paddasslem15  36852  4atex  37094  trlval4  37206  cdlemc5  37213  cdlemc6  37214  cdlemd2  37217  cdlemd3  37218  cdlemd4  37219  cdleme0moN  37243  cdleme3g  37252  cdleme3h  37253  cdleme3  37255  cdleme11g  37283  cdleme11h  37284  cdleme11j  37285  cdleme11k  37286  cdleme11l  37287  cdleme11  37288  cdleme14  37291  cdleme15a  37292  cdleme15c  37294  cdleme15d  37295  cdleme15  37296  cdleme16b  37297  cdleme16c  37298  cdleme16d  37299  cdleme16e  37300  cdleme16f  37301  cdleme18a  37309  cdleme18b  37310  cdleme18c  37311  cdleme19b  37322  cdleme19e  37325  cdleme20bN  37328  cdleme20c  37329  cdleme20d  37330  cdleme20e  37331  cdleme20f  37332  cdleme20g  37333  cdleme20h  37334  cdleme20j  37336  cdleme20l2  37339  cdleme20l  37340  cdleme20m  37341  cdleme21ct  37347  cdleme22d  37361  cdleme22e  37362  cdleme22eALTN  37363  cdleme26e  37377  cdleme27a  37385  cdleme28a  37388  cdleme30a  37396  cdleme43fsv1snlem  37438  cdlemefs44  37444  cdlemefs45ee  37448  cdleme35sn2aw  37476  cdleme36a  37478  cdleme39n  37484  cdleme40m  37485  cdleme42k  37502  cdlemeg47rv2  37528  cdlemeg46frv  37543  cdlemeg46vrg  37545  cdlemeg46rgv  37546  cdlemeg46req  37547  cdlemg2fv2  37618  cdlemg4g  37634  cdlemg4  37635  cdlemg6c  37638  cdlemg8b  37646  cdlemg8c  37647  cdlemg9a  37650  cdlemg9b  37651  cdlemg9  37652  cdlemg12a  37661  cdlemg12b  37662  cdlemg12c  37663  cdlemg17h  37686  cdlemg18b  37697  cdlemg18c  37698  cdlemg31b0a  37713  cdlemg27b  37714  cdlemg31d  37718  cdlemg28b  37721  cdlemg33a  37724  cdlemg33b  37725  cdlemg33c  37726  cdlemg33d  37727  cdlemg33e  37728  cdlemg33  37729  cdlemh  37835  cdlemk6  37855  cdlemki  37859  cdlemksat  37864  cdlemksv2  37865  cdlemk7  37866  cdlemk11  37867  cdlemk12  37868  cdlemkole  37871  cdlemk14  37872  cdlemk15  37873  cdlemk17  37876  cdlemk1u  37877  cdlemk5u  37879  cdlemk6u  37880  cdlemk7u  37888  cdlemk11u  37889  cdlemk12u  37890  cdlemk7u-2N  37906  cdlemk11u-2N  37907  cdlemk12u-2N  37908  cdlemk20-2N  37910  cdlemk28-3  37926  cdlemk33N  37927  cdlemk34  37928  cdlemk37  37932  cdlemk39  37934  cdlemk35s  37955  cdlemk39s  37957  cdlemk47  37967  cdlemk48  37968  cdlemk50  37970  cdlemk51  37971  cdlemk52  37972  cdlemkyyN  37980  cdlemk43N  37981  cdlemn2  38213  cdlemn10  38224
  Copyright terms: Public domain W3C validator