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

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

Proof of Theorem simp22
StepHypRef Expression
1 simp2 1060 . 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:  simpl22  1138  simpr22  1147  simp122  1192  simp222  1201  simp322  1210  elfiun  8280  cofsmo  9035  modexp  12939  funcoppc  16456  funcres  16477  catcisolem  16677  1stfcl  16758  2ndfcl  16759  prfcl  16764  evlfcl  16783  curf1cl  16789  curfcl  16793  hofcl  16820  mulgdirlem  17493  pmtrprfv3  17795  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  ogrpsub  29502  ogrpaddlt  29503  ogrpsublt  29507  rhmdvd  29606  bnj966  30722  mclspps  31189  cgrtr  31741  cgrtr3  31743  ofscom  31756  cgrextend  31757  btwnxfr  31805  colinearxfr  31824  lineext  31825  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  linecom  31899  eqlkr  33866  lshpkrlem5  33881  omlmod1i2N  34027  cvrnbtwn3  34043  cvrcmp2  34051  cvlexch2  34096  cvlexchb2  34098  cvlatexchb2  34102  cvlatexch1  34103  cvlatexch2  34104  cvlatexch3  34105  cvlsupr7  34115  cvlsupr8  34116  atnlej1  34145  atnlej2  34146  2llnneN  34175  cvratlem  34187  atcvrneN  34196  atlelt  34204  2atjm  34211  3noncolr2  34215  3noncolr1N  34216  hlatcon2  34218  3dimlem2  34225  3dim1  34233  3dim2  34234  1cvrat  34242  ps-1  34243  ps-2  34244  2atjlej  34245  hlatexch3N  34246  ps-2b  34248  3atlem1  34249  3atlem5  34253  3atlem6  34254  2atm  34293  ps-2c  34294  lplni2  34303  lplnri3N  34321  llncvrlpln2  34323  2atmat  34327  2llnm2N  34334  2llnm3N  34335  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  paddasslem16  34601  pmodlem1  34612  pmod2iN  34615  hlmod1i  34622  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  osumcllem7N  34728  osumcllem9N  34730  pl42lem1N  34745  4atexlemswapqr  34829  4atex2  34843  4atex2-0bOLDN  34845  trlval4  34955  cdlemc5  34962  cdlemc6  34963  cdlemd2  34966  cdlemd4  34968  cdlemd6  34970  cdleme00a  34976  cdleme0e  34984  cdleme4  35005  cdleme4a  35006  cdleme5  35007  cdleme9  35020  cdleme16aN  35026  cdleme11c  35028  cdleme11dN  35029  cdleme11e  35030  cdleme11g  35032  cdleme11h  35033  cdleme11j  35034  cdleme11k  35035  cdleme11l  35036  cdleme11  35037  cdleme12  35038  cdleme13  35039  cdleme14  35040  cdleme15a  35041  cdleme15c  35043  cdleme16b  35046  cdleme16c  35047  cdleme16d  35048  cdleme16e  35049  cdleme16f  35050  cdleme17d1  35056  cdleme0nex  35057  cdleme18a  35058  cdleme18b  35059  cdleme18c  35060  cdleme18d  35062  cdlemednpq  35066  cdlemednuN  35067  cdleme20zN  35068  cdleme20y  35069  cdleme20yOLD  35070  cdleme19a  35071  cdleme19b  35072  cdleme19d  35074  cdleme19e  35075  cdleme20aN  35077  cdleme20d  35080  cdleme20f  35082  cdleme20g  35083  cdleme20i  35085  cdleme20j  35086  cdleme20l1  35088  cdleme20l2  35089  cdleme20l  35090  cdleme20m  35091  cdleme21b  35094  cdleme21c  35095  cdleme21e  35099  cdleme21j  35104  cdleme22aa  35107  cdleme22a  35108  cdleme22b  35109  cdleme22cN  35110  cdleme22d  35111  cdleme22e  35112  cdleme22eALTN  35113  cdleme22f  35114  cdleme26fALTN  35130  cdleme26f  35131  cdleme26f2ALTN  35132  cdleme26f2  35133  cdleme27N  35137  cdleme28a  35138  cdleme28b  35139  cdleme30a  35146  cdlemefs31fv1  35192  cdleme32b  35210  cdleme32c  35211  cdleme32e  35213  cdleme35h  35224  cdleme36a  35228  cdleme36m  35229  cdleme41sn3aw  35242  cdleme41sn4aw  35243  cdleme41fva11  35245  cdleme42k  35252  cdleme43cN  35259  cdleme46f2g1  35262  cdlemeg46fjgN  35289  cdlemeg46fjv  35291  cdlemeg46frv  35293  cdlemeg46rgv  35296  cdlemeg46req  35297  cdlemeg46gfv  35298  cdleme50trn2a  35318  cdlemg4a  35376  cdlemg4d  35381  cdlemg4e  35382  cdlemg4f  35383  cdlemg8c  35397  cdlemg9a  35400  cdlemg9b  35401  cdlemg10a  35408  cdlemg10  35409  cdlemg12b  35412  cdlemg12f  35416  cdlemg12g  35417  cdlemg12  35418  cdlemg17dN  35431  cdlemg17dALTN  35432  cdlemg17e  35433  cdlemg17f  35434  cdlemg17g  35435  cdlemg17i  35437  cdlemg17ir  35438  cdlemg17pq  35440  cdlemg17bq  35441  cdlemg17iqN  35442  cdlemg17  35445  cdlemg18b  35447  cdlemg18c  35448  cdlemg18d  35449  cdlemg18  35450  cdlemg19  35452  cdlemg21  35454  cdlemg28a  35461  cdlemg31b0a  35463  cdlemg27b  35464  cdlemg33b0  35469  cdlemg28b  35471  cdlemg28  35472  cdlemg35  35481  cdlemg36  35482  cdlemg44a  35499  cdlemh  35585  cdlemi2  35587  cdlemj1  35589  tendocan  35592  cdlemk5a  35603  cdlemk5  35604  cdlemki  35609  cdlemkvcl  35610  cdlemk10  35611  cdlemksv2  35615  cdlemk7  35616  cdlemk11  35617  cdlemk12  35618  cdlemkoatnle  35619  cdlemk15  35623  cdlemk16a  35624  cdlemk16  35625  cdlemk1u  35627  cdlemk5u  35629  cdlemk6u  35630  cdlemk18  35636  cdlemk19  35637  cdlemk7u  35638  cdlemk11u  35639  cdlemk12u  35640  cdlemk21N  35641  cdlemk20  35642  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  cdlemk22  35661  cdlemk30  35662  cdlemkuel-3  35666  cdlemkuv2-3N  35667  cdlemk18-3N  35668  cdlemkfid1N  35689  cdlemkid1  35690  cdlemkfid3N  35693  cdlemky  35694  cdlemk11ta  35697  cdlemk47  35717  cdlemk48  35718  cdlemk49  35719  cdlemk50  35720  cdlemk51  35721  cdlemk52  35722  cdlemk53a  35723  cdlemk53  35725  cdlemk54  35726  cdlemk55a  35727  cdlemkyyN  35730  cdlemk43N  35731  cdlemk55u1  35733  cdlemk55u  35734  cdlemk39u1  35735  cdlemk19u1  35737  cdleml1N  35744  cdleml2N  35745  cdleml3N  35746  dia2dimlem6  35838  cdlemn2  35964  cdlemn2a  35965  cdlemn5pre  35969  cdlemn11a  35976  dihjustlem  35985  dihjust  35986  dihmeetlem15N  36090  lclkrlem2y  36300  relexpmulnn  37482  amgmwlem  41851
  Copyright terms: Public domain W3C validator