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

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

Proof of Theorem simp23l
StepHypRef Expression
1 simp3l 1198 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant2 1131 1 ((𝜏 ∧ (𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  ax5seglem6  26732  lshpkrlem5  36409  lplnexllnN  36859  4atexlemt  37348  4atex2  37372  4atex3  37376  trlval4  37483  cdlemc5  37490  cdlemc6  37491  cdlemd2  37494  cdleme0e  37512  cdleme0moN  37520  cdleme3g  37529  cdleme3h  37530  cdleme3  37532  cdleme4  37533  cdleme5  37535  cdleme9  37548  cdleme11fN  37559  cdleme11j  37562  cdleme11k  37563  cdleme11l  37564  cdleme11  37565  cdleme14  37568  cdleme15a  37569  cdleme15b  37570  cdleme15c  37571  cdleme16b  37574  cdleme16c  37575  cdleme16d  37576  cdleme16e  37577  cdleme16f  37578  cdleme17d1  37584  cdleme18c  37588  cdlemednpq  37594  cdleme19c  37600  cdleme20bN  37605  cdleme20d  37607  cdleme20f  37609  cdleme20g  37610  cdleme20h  37611  cdleme20j  37613  cdleme20l2  37616  cdleme20l  37617  cdleme20m  37618  cdleme22cN  37637  cdleme22d  37638  cdleme22e  37639  cdleme22f  37641  cdleme26fALTN  37657  cdleme26f  37658  cdleme26f2ALTN  37659  cdleme26f2  37660  cdleme27a  37662  cdleme28a  37665  cdlemefs44  37721  cdlemefs45ee  37725  cdleme32b  37737  cdleme32c  37738  cdleme32e  37740  cdleme35sn2aw  37753  cdleme37m  37757  cdleme39n  37761  cdleme40n  37763  cdleme40w  37765  cdleme42k  37779  cdlemeg47rv2  37805  cdlemeg46rjgN  37817  cdlemeg46rgv  37823  cdlemeg46req  37824  cdlemg2fv2  37895  cdlemg17h  37963  cdlemg31b0a  37990  cdlemg27b  37991  cdlemg31d  37995  cdlemg28b  37998  cdlemg28  37999  cdlemg29  38000  cdlemg33a  38001  cdlemg33b  38002  cdlemg33c  38003  cdlemg33d  38004  cdlemg33e  38005  cdlemg44a  38026  cdlemk7u-2N  38183  cdlemk11u-2N  38184  cdlemk12u-2N  38185  cdlemk26-3  38201  cdlemk27-3  38202  cdlemkfid3N  38220  cdlemn2  38490  cdlemn10  38501  cdlemn11c  38504
  Copyright terms: Public domain W3C validator