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

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

Proof of Theorem simp23l
StepHypRef Expression
1 simp3l 1243 . 2 ((𝜒𝜃 ∧ (𝜑𝜓)) → 𝜑)
213ad2ant2 1128 1 ((𝜏 ∧ (𝜒𝜃 ∧ (𝜑𝜓)) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  ax5seglem6  26035  lshpkrlem5  34923  lplnexllnN  35372  4atexlemt  35861  4atex2  35885  4atex3  35889  trlval4  35997  cdlemc5  36004  cdlemc6  36005  cdlemd2  36008  cdleme0e  36026  cdleme0moN  36034  cdleme3g  36043  cdleme3h  36044  cdleme3  36046  cdleme4  36047  cdleme5  36049  cdleme9  36062  cdleme11fN  36073  cdleme11j  36076  cdleme11k  36077  cdleme11l  36078  cdleme11  36079  cdleme14  36082  cdleme15a  36083  cdleme15b  36084  cdleme15c  36085  cdleme16b  36088  cdleme16c  36089  cdleme16d  36090  cdleme16e  36091  cdleme16f  36092  cdleme17d1  36098  cdleme18c  36102  cdlemednpq  36108  cdleme19c  36114  cdleme20bN  36119  cdleme20d  36121  cdleme20f  36123  cdleme20g  36124  cdleme20h  36125  cdleme20j  36127  cdleme20l2  36130  cdleme20l  36131  cdleme20m  36132  cdleme22cN  36151  cdleme22d  36152  cdleme22e  36153  cdleme22f  36155  cdleme26fALTN  36171  cdleme26f  36172  cdleme26f2ALTN  36173  cdleme26f2  36174  cdleme27a  36176  cdleme28a  36179  cdlemefs44  36235  cdlemefs45ee  36239  cdleme32b  36251  cdleme32c  36252  cdleme32e  36254  cdleme35sn2aw  36267  cdleme37m  36271  cdleme39n  36275  cdleme40n  36277  cdleme40w  36279  cdleme42k  36293  cdlemeg47rv2  36319  cdlemeg46rjgN  36331  cdlemeg46rgv  36337  cdlemeg46req  36338  cdlemg2fv2  36409  cdlemg17h  36477  cdlemg31b0a  36504  cdlemg27b  36505  cdlemg31d  36509  cdlemg28b  36512  cdlemg28  36513  cdlemg29  36514  cdlemg33a  36515  cdlemg33b  36516  cdlemg33c  36517  cdlemg33d  36518  cdlemg33e  36519  cdlemg44a  36540  cdlemk7u-2N  36697  cdlemk11u-2N  36698  cdlemk12u-2N  36699  cdlemk26-3  36715  cdlemk27-3  36716  cdlemkfid3N  36734  cdlemn2  37005  cdlemn10  37016  cdlemn11c  37019
  Copyright terms: Public domain W3C validator