Theorem simp12 1212

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp12	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Proof of Theorem simp12

Step	Hyp	Ref	Expression
1		simp2 1144	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	3ad2ant1 1140	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  simp112  1311  simp212  1320  simp312  1329  dvdsgcd  16508  coprimeprodsq  16774  pythagtriplem4  16785  pythagtriplem13  16793  pythagtriplem14  16794  pythagtriplem16  16796  pythagtrip  16800  pceu  16812  mremre  17561  lsmpropd  19647  m2cpminvid  22740  decpmatid  22757  mply1topmatcllem  22790  cmpsublem  23386  isfil2  23843  cxple2a  26685  isosctr  26807  nolesgn2o  27657  nolesgn2ores  27658  nogesgn1o  27659  nogesgn1ores  27660  nolt02o  27681  nogt01o  27682  sltstr  27801  cofslts  27932  coinitslts  27933  cofcut2  27936  onsfi  28370  brbtwn2  28996  colinearalg  29001  ax5seg  29029  axcontlem4  29058  bayesth  34635  bnj1204  35209  bnj1279  35215  ofscom  36250  btwndiff  36270  ifscgr  36287  brofs2  36320  brifs2  36321  fscgr  36323  btwnconn1lem1  36330  btwnconn1lem2  36331  btwnconn1lem3  36332  btwnconn1lem4  36333  btwnconn1lem12  36341  seglecgr12im  36353  seglecgr12  36354  ivthALT  36578  islshpcv  39560  lkrshp  39612  lshpsmreu  39616  lshpkrlem5  39621  cvrval3  39920  4noncolr3  39960  4noncolr2  39961  4noncolr1  39962  athgt  39963  3dimlem2  39966  3dimlem3a  39967  3dimlem4a  39970  3dimlem4  39971  3dimlem4OLDN  39972  1cvratex  39980  hlatexch4  39988  ps-2b  39989  3atlem4  39993  llnnleat  40020  2atm  40034  ps-2c  40035  llnmlplnN  40046  lplnnlelln  40050  2atmat  40068  lvoli2  40088  lvolnlelln  40091  4atlem3b  40105  4atlem10  40113  4atlem11a  40114  4atlem11b  40115  4atlem12a  40117  lplncvrlvol2  40122  2lplnja  40126  dalemswapyz  40163  lneq2at  40285  2lnat  40291  cdlema1N  40298  cdlemb  40301  paddasslem15  40341  pmodlem1  40353  llnmod2i2  40370  llnexchb2lem  40375  dalawlem1  40378  dalawlem3  40380  dalawlem4  40381  dalawlem6  40383  dalawlem7  40384  dalawlem9  40386  dalawlem10  40387  dalawlem11  40388  dalawlem12  40389  dalawlem13  40390  dalawlem15  40392  osumcllem5N  40467  osumcllem6N  40468  osumcllem7N  40469  osumcllem9N  40471  osumcllem10N  40472  osumcllem11N  40473  pl42lem1N  40486  lhpmcvr5N  40534  lhp2atne  40541  lhp2at0ne  40543  4atexlempw  40556  4atexlemex6  40581  4atexlem7  40582  ldilco  40623  ltrneq  40656  trlval2  40670  trlnidat  40680  cdlemd7  40711  cdleme7aa  40749  cdleme7c  40752  cdleme7d  40753  cdleme7e  40754  cdleme7ga  40755  cdleme7  40756  cdleme11c  40768  cdleme11e  40770  cdleme11l  40776  cdleme11  40777  cdleme14  40780  cdleme15a  40781  cdleme15c  40783  cdleme16b  40786  cdleme16c  40787  cdleme16d  40788  cdleme16e  40789  cdleme16f  40790  cdleme0nex  40797  cdleme18d  40802  cdleme19b  40811  cdleme19d  40813  cdleme19e  40814  cdleme20f  40821  cdleme20k  40826  cdleme20l1  40827  cdleme20l2  40828  cdleme20l  40829  cdleme20m  40830  cdleme21a  40832  cdleme21b  40833  cdleme21ct  40836  cdleme21d  40837  cdleme21e  40838  cdleme21f  40839  cdleme21h  40841  cdleme21i  40842  cdleme22eALTN  40852  cdleme22f2  40854  cdleme22g  40855  cdleme24  40859  cdleme25a  40860  cdleme25c  40862  cdleme25dN  40863  cdleme26e  40866  cdleme26ee  40867  cdleme26eALTN  40868  cdleme27N  40876  cdleme28a  40877  cdleme28b  40878  cdleme28  40880  cdlemefr32sn2aw  40911  cdlemefs32sn1aw  40921  cdleme43fsv1snlem  40927  cdleme41sn3a  40940  cdleme32c  40950  cdleme32e  40952  cdleme32le  40954  cdleme35a  40955  cdleme35b  40957  cdleme35c  40958  cdleme35e  40960  cdleme35f  40961  cdleme36a  40967  cdleme36m  40968  cdleme39a  40972  cdleme40m  40974  cdleme40n  40975  cdleme43bN  40997  cdleme43dN  40999  cdleme46f2g2  41000  cdleme46f2g1  41001  cdleme17d2  41002  cdleme4gfv  41014  cdlemeg49le  41018  cdlemeg46c  41020  cdlemeg46fvaw  41023  cdlemeg46nlpq  41024  cdlemeg46gfre  41039  cdleme50trn2  41058  cdleme  41067  cdlemg2idN  41103  cdlemg7fvbwN  41114  cdlemg10bALTN  41143  cdlemg10a  41147  cdlemg12d  41153  cdlemg12g  41156  cdlemg12  41157  cdlemg13a  41158  cdlemg13  41159  cdlemg17b  41169  cdlemg17dN  41170  cdlemg17dALTN  41171  cdlemg17e  41172  cdlemg17f  41173  cdlemg17i  41176  cdlemg17pq  41179  cdlemg17bq  41180  cdlemg17iqN  41181  cdlemg18d  41188  cdlemg18  41189  cdlemg19a  41190  cdlemg19  41191  cdlemg21  41193  cdlemg27a  41199  cdlemg28a  41200  cdlemg31b0N  41201  cdlemg27b  41203  cdlemg31c  41206  cdlemg33b0  41208  cdlemg33c0  41209  cdlemg28  41211  cdlemg33a  41213  cdlemg33  41218  cdlemg36  41221  ltrnco  41226  cdlemg44  41240  cdlemg47  41243  tendococl  41279  tendoplcl  41288  cdlemh1  41322  cdlemh2  41323  cdlemh  41324  cdlemi  41327  tendocan  41331  cdlemk5  41343  cdlemk6  41344  cdlemk7  41355  cdlemk11  41356  cdlemk12  41357  cdlemkole  41360  cdlemk14  41361  cdlemk15  41362  cdlemk16a  41363  cdlemk16  41364  cdlemk18  41375  cdlemk19  41376  cdlemk7u  41377  cdlemk11u  41378  cdlemk12u  41379  cdlemk21N  41380  cdlemk20  41381  cdlemkoatnle-2N  41382  cdlemk13-2N  41383  cdlemkole-2N  41384  cdlemk14-2N  41385  cdlemk15-2N  41386  cdlemk16-2N  41387  cdlemk17-2N  41388  cdlemk18-2N  41393  cdlemk19-2N  41394  cdlemk7u-2N  41395  cdlemk11u-2N  41396  cdlemk12u-2N  41397  cdlemk21-2N  41398  cdlemk20-2N  41399  cdlemk22  41400  cdlemk27-3  41414  cdlemk33N  41416  cdlemk11ta  41436  cdlemkid3N  41440  cdlemk11tc  41452  cdlemk11t  41453  cdlemk45  41454  cdlemk46  41455  cdlemk47  41456  cdlemk48  41457  cdlemk49  41458  cdlemk50  41459  cdlemk51  41460  cdlemk52  41461  cdlemk53a  41462  cdlemk55b  41467  cdlemkyyN  41469  cdlemk55u1  41472  cdlemk39u1  41474  cdlemk56  41478  cdlemm10N  41625  dihord1  41725  dihord2a  41726  dihord2b  41727  dihord10  41730  dihord4  41765  dihord5apre  41769  dihglblem2N  41801  dihjatc1  41818  dihjatc2N  41819  dihjatc3  41820  dihmeetlem15N  41828  dihmeetlem20N  41833  mapdpglem24  42211  hdmap14lem11  42385  hdmap14lem12  42386  flt4lem5  43115  mzpsubst  43212  monotuz  43401  congmul  43427  congsub  43430  ntrclsiso  44526  ntrclskb  44528  ntrclsk3  44529  infleinf  45830  mullimc  46075  mullimcf  46082  0ellimcdiv  46106  limclner  46108  sge0xaddlem2  46891  isubgr3stgrlem3  48473  lincdifsn  48929  itschlc0yqe  49265  itscnhlc0xyqsol  49270  itsclc0xyqsolr  49274  itsclquadeu  49282