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

Theorem simp21 1092
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp21 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp21
StepHypRef Expression
1 simp1 1059 . 2 ((𝜓𝜒𝜃) → 𝜓)
213ad2ant2 1081 1 ((𝜑 ∧ (𝜓𝜒𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  simpl21  1137  simpr21  1146  simp121  1191  simp221  1200  simp321  1209  omeulem1  7607  cofsmo  9035  axdc4lem  9221  0catg  16269  funcoppc  16456  funcres  16477  catcisolem  16677  1stfcl  16758  2ndfcl  16759  prfcl  16764  evlfcl  16783  curf1cl  16789  curfcl  16793  hofcl  16820  mulgdirlem  17493  mdetunilem4  20340  mdetuni0  20346  mdetmul  20348  prdsxmetlem  22083  isosctrlem3  24450  isosctr  24451  amgmlem  24616  f1otrg  25651  colinearalg  25690  ax5seglem6  25714  ax5seg  25718  axpasch  25721  axeuclidlem  25742  axeuclid  25743  uhgr2edg  25993  ogrpsub  29502  ogrpaddlt  29503  ogrpsublt  29507  rhmdvd  29606  bnj1128  30766  mclspps  31189  cgrtr  31741  cgrtr3  31743  ofscom  31756  segconeq  31759  ifscgr  31793  btwnxfr  31805  colinearxfr  31824  lineext  31825  brofs2  31826  brifs2  31827  fscgr  31829  linecgr  31830  btwnconn1lem1  31836  btwnconn1lem2  31837  btwnconn1lem3  31838  btwnconn1lem4  31839  btwnconn1lem5  31840  btwnconn1lem6  31841  btwnconn1lem7  31842  seglecgr12im  31859  seglecgr12  31860  segletr  31863  broutsideof3  31875  outsideofeq  31879  lineunray  31896  lineelsb2  31897  linecom  31899  lshpkrlem5  33881  omlmod1i2N  34027  cvrnbtwn3  34043  cvrcmp  34050  cvrcmp2  34051  cvlexch2  34096  cvlexchb2  34098  cvlatexchb2  34102  cvlatexch2  34104  cvlatexch3  34105  cvlsupr7  34115  atnlej1  34145  atnlej2  34146  2llnneN  34175  cvratlem  34187  atcvrneN  34196  atcvrj1  34197  atlelt  34204  2atjm  34211  3noncolr2  34215  3noncolr1N  34216  3dimlem2  34225  3dim1  34233  3dim2  34234  1cvrat  34242  ps-1  34243  ps-2  34244  2atjlej  34245  hlatexch3N  34246  ps-2b  34248  3atlem1  34249  3atlem2  34250  3atlem5  34253  3atlem6  34254  llnle  34284  2atm  34293  ps-2c  34294  lplni2  34303  lplnle  34306  lplnnle2at  34307  lplnri3N  34321  llncvrlpln2  34323  2atmat  34327  2llnm2N  34334  2llnm4  34336  2llnmeqat  34337  lvolnle3at  34348  4atlem0ae  34360  4atlem0be  34361  4atlem3b  34364  4atlem9  34369  4atlem10a  34370  4atlem10  34372  4atlem11a  34373  4atlem12a  34376  4at2  34380  2lplnm2N  34387  lneq2at  34544  2llnma1b  34552  2llnma1  34553  2llnma3r  34554  2llnma2  34555  2llnma2rN  34556  cdlema1N  34557  paddasslem2  34587  paddasslem15  34600  paddasslem16  34601  pmodlem1  34612  pmodlem2  34613  pmod2iN  34615  hlmod1i  34622  atmod1i1m  34624  atmod2i1  34627  atmod2i2  34628  atmod3i1  34630  atmod3i2  34631  atmod4i1  34632  atmod4i2  34633  llnexchb2lem  34634  llnexch2N  34636  dalawlem3  34639  dalawlem4  34640  dalawlem5  34641  dalawlem6  34642  dalawlem7  34643  dalawlem8  34644  dalawlem9  34645  dalawlem11  34647  dalawlem12  34648  dalawlem13  34649  dalawlem15  34651  osumcllem9N  34730  pl42lem1N  34745  4atexlems  34818  4atex2  34843  4atex2-0bOLDN  34845  trlval4  34955  cdlemc5  34962  cdlemc6  34963  cdlemd2  34966  cdlemd4  34968  cdlemd6  34970  cdleme00a  34976  cdleme0e  34984  cdleme3g  35001  cdleme3h  35002  cdleme3  35004  cdleme4  35005  cdleme4a  35006  cdleme5  35007  cdleme9  35020  cdleme16aN  35026  cdleme11c  35028  cdleme11e  35030  cdleme11g  35032  cdleme11h  35033  cdleme11j  35034  cdleme11k  35035  cdleme11l  35036  cdleme11  35037  cdleme12  35038  cdleme14  35040  cdleme15c  35043  cdleme16b  35046  cdleme16c  35047  cdleme16d  35048  cdleme16e  35049  cdleme16f  35050  cdleme0nex  35057  cdleme18a  35058  cdleme18c  35060  cdleme18d  35062  cdlemednpq  35066  cdlemednuN  35067  cdleme20zN  35068  cdleme20y  35069  cdleme20yOLD  35070  cdleme19a  35071  cdleme19b  35072  cdleme19d  35074  cdleme19e  35075  cdleme20aN  35077  cdleme20bN  35078  cdleme20c  35079  cdleme20d  35080  cdleme20f  35082  cdleme20g  35083  cdleme20i  35085  cdleme20j  35086  cdleme20l1  35088  cdleme20l2  35089  cdleme20l  35090  cdleme20m  35091  cdleme21b  35094  cdleme21c  35095  cdleme21e  35099  cdleme21f  35100  cdleme22a  35108  cdleme22b  35109  cdleme22e  35112  cdleme22eALTN  35113  cdleme22f  35114  cdleme26eALTN  35129  cdleme26fALTN  35130  cdleme26f  35131  cdleme26f2ALTN  35132  cdleme26f2  35133  cdleme27N  35137  cdleme28a  35138  cdleme28b  35139  cdleme30a  35146  cdleme43fsv1snlem  35188  cdlemefs31fv1  35192  cdlemefs45eN  35199  cdleme32b  35210  cdleme32c  35211  cdleme32d  35212  cdleme35h  35224  cdleme36a  35228  cdleme36m  35229  cdleme37m  35230  cdleme40m  35235  cdleme40n  35236  cdleme41sn3aw  35242  cdleme41sn4aw  35243  cdleme41fva11  35245  cdleme42k  35252  cdleme43cN  35259  cdleme43dN  35260  cdleme46f2g1  35262  cdlemeg47rv2  35278  cdlemeg46sfg  35288  cdlemeg46fjgN  35289  cdlemeg46rjgN  35290  cdlemeg46fjv  35291  cdlemeg46frv  35293  cdlemeg46vrg  35295  cdlemeg46rgv  35296  cdlemeg46req  35297  cdlemeg46gfv  35298  cdlemg4a  35376  cdlemg4d  35381  cdlemg4e  35382  cdlemg4f  35383  cdlemg4g  35384  cdlemg4  35385  cdlemg6d  35389  cdlemg6e  35390  cdlemg8b  35396  cdlemg8c  35397  cdlemg9a  35400  cdlemg9b  35401  cdlemg10a  35408  cdlemg10  35409  cdlemg12a  35411  cdlemg12b  35412  cdlemg12f  35416  cdlemg12g  35417  cdlemg12  35418  cdlemg17dN  35431  cdlemg17dALTN  35432  cdlemg17e  35433  cdlemg17f  35434  cdlemg17g  35435  cdlemg17h  35436  cdlemg17i  35437  cdlemg17pq  35440  cdlemg17iqN  35442  cdlemg17  35445  cdlemg18b  35447  cdlemg18c  35448  cdlemg19a  35451  cdlemg19  35452  cdlemg28a  35461  cdlemg27b  35464  cdlemg28b  35471  cdlemg28  35472  cdlemg33a  35474  cdlemg33b  35475  cdlemg33c  35476  cdlemg33d  35477  cdlemg33e  35478  cdlemg33  35479  cdlemg35  35481  cdlemg36  35482  cdlemg44a  35499  cdlemh  35585  cdlemi2  35587  cdlemj1  35589  tendocan  35592  cdlemk5a  35603  cdlemki  35609  cdlemkvcl  35610  cdlemk10  35611  cdlemksv2  35615  cdlemkole  35621  cdlemk14  35622  cdlemk15  35623  cdlemk16a  35624  cdlemk16  35625  cdlemk17  35626  cdlemk18  35636  cdlemk19  35637  cdlemkoatnle-2N  35643  cdlemk13-2N  35644  cdlemkole-2N  35645  cdlemk14-2N  35646  cdlemk15-2N  35647  cdlemk16-2N  35648  cdlemk17-2N  35649  cdlemk18-2N  35654  cdlemk19-2N  35655  cdlemk30  35662  cdlemk18-3N  35668  cdlemk23-3  35670  cdlemk25-3  35672  cdlemk27-3  35675  cdlemk37  35682  cdlemkfid1N  35689  cdlemkid1  35690  cdlemky  35694  cdlemk11ta  35697  cdlemk47  35717  cdlemk48  35718  cdlemk49  35719  cdlemk50  35720  cdlemk51  35721  cdlemk52  35722  cdlemk53a  35723  cdlemk54  35726  cdlemk39u1  35735  cdlemk19u1  35737  cdleml1N  35744  cdleml2N  35745  cdleml3N  35746  dia2dimlem6  35838  cdlemn2  35964  cdlemn2a  35965  cdlemn5pre  35969  cdlemn10  35975  cdlemn11c  35978  cdlemn11pre  35979  dihjustlem  35985  dihjust  35986  lclkrlem2y  36300  relexpmulnn  37482  lincreslvec3  41559  amgmwlem  41851
  Copyright terms: Public domain W3C validator