Theorem simp12 1204

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 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	3ad2ant1 1133	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simp112  1303  simp212  1312  simp312  1321  dvdsgcd  16436  coprimeprodsq  16691  pythagtriplem4  16702  pythagtriplem13  16710  pythagtriplem14  16711  pythagtriplem16  16713  pythagtrip  16717  pceu  16729  mremre  17498  lsmpropd  19473  m2cpminvid  22139  decpmatid  22156  mply1topmatcllem  22189  cmpsublem  22787  isfil2  23244  cxple2a  26091  isosctr  26208  nolesgn2o  27056  nolesgn2ores  27057  nogesgn1o  27058  nogesgn1ores  27059  nolt02o  27080  nogt01o  27081  sslttr  27189  cofsslt  27280  coinitsslt  27281  cofcut2  27284  brbtwn2  27917  colinearalg  27922  ax5seg  27950  axcontlem4  27979  bayesth  33128  bnj1204  33713  bnj1279  33719  ofscom  34668  btwndiff  34688  ifscgr  34705  brofs2  34738  brifs2  34739  fscgr  34741  btwnconn1lem1  34748  btwnconn1lem2  34749  btwnconn1lem3  34750  btwnconn1lem4  34751  btwnconn1lem12  34759  seglecgr12im  34771  seglecgr12  34772  ivthALT  34883  islshpcv  37588  lkrshp  37640  lshpsmreu  37644  lshpkrlem5  37649  cvrval3  37949  4noncolr3  37989  4noncolr2  37990  4noncolr1  37991  athgt  37992  3dimlem2  37995  3dimlem3a  37996  3dimlem4a  37999  3dimlem4  38000  3dimlem4OLDN  38001  1cvratex  38009  hlatexch4  38017  ps-2b  38018  3atlem4  38022  llnnleat  38049  2atm  38063  ps-2c  38064  llnmlplnN  38075  lplnnlelln  38079  2atmat  38097  lvoli2  38117  lvolnlelln  38120  4atlem3b  38134  4atlem10  38142  4atlem11a  38143  4atlem11b  38144  4atlem12a  38146  lplncvrlvol2  38151  2lplnja  38155  dalemswapyz  38192  lneq2at  38314  2lnat  38320  cdlema1N  38327  cdlemb  38330  paddasslem15  38370  pmodlem1  38382  llnmod2i2  38399  llnexchb2lem  38404  dalawlem1  38407  dalawlem3  38409  dalawlem4  38410  dalawlem6  38412  dalawlem7  38413  dalawlem9  38415  dalawlem10  38416  dalawlem11  38417  dalawlem12  38418  dalawlem13  38419  dalawlem15  38421  osumcllem5N  38496  osumcllem6N  38497  osumcllem7N  38498  osumcllem9N  38500  osumcllem10N  38501  osumcllem11N  38502  pl42lem1N  38515  lhpmcvr5N  38563  lhp2atne  38570  lhp2at0ne  38572  4atexlempw  38585  4atexlemex6  38610  4atexlem7  38611  ldilco  38652  ltrneq  38685  trlval2  38699  trlnidat  38709  cdlemd7  38740  cdleme7aa  38778  cdleme7c  38781  cdleme7d  38782  cdleme7e  38783  cdleme7ga  38784  cdleme7  38785  cdleme11c  38797  cdleme11e  38799  cdleme11l  38805  cdleme11  38806  cdleme14  38809  cdleme15a  38810  cdleme15c  38812  cdleme16b  38815  cdleme16c  38816  cdleme16d  38817  cdleme16e  38818  cdleme16f  38819  cdleme0nex  38826  cdleme18d  38831  cdleme19b  38840  cdleme19d  38842  cdleme19e  38843  cdleme20f  38850  cdleme20k  38855  cdleme20l1  38856  cdleme20l2  38857  cdleme20l  38858  cdleme20m  38859  cdleme21a  38861  cdleme21b  38862  cdleme21ct  38865  cdleme21d  38866  cdleme21e  38867  cdleme21f  38868  cdleme21h  38870  cdleme21i  38871  cdleme22eALTN  38881  cdleme22f2  38883  cdleme22g  38884  cdleme24  38888  cdleme25a  38889  cdleme25c  38891  cdleme25dN  38892  cdleme26e  38895  cdleme26ee  38896  cdleme26eALTN  38897  cdleme27N  38905  cdleme28a  38906  cdleme28b  38907  cdleme28  38909  cdlemefr32sn2aw  38940  cdlemefs32sn1aw  38950  cdleme43fsv1snlem  38956  cdleme41sn3a  38969  cdleme32c  38979  cdleme32e  38981  cdleme32le  38983  cdleme35a  38984  cdleme35b  38986  cdleme35c  38987  cdleme35e  38989  cdleme35f  38990  cdleme36a  38996  cdleme36m  38997  cdleme39a  39001  cdleme40m  39003  cdleme40n  39004  cdleme43bN  39026  cdleme43dN  39028  cdleme46f2g2  39029  cdleme46f2g1  39030  cdleme17d2  39031  cdleme4gfv  39043  cdlemeg49le  39047  cdlemeg46c  39049  cdlemeg46fvaw  39052  cdlemeg46nlpq  39053  cdlemeg46gfre  39068  cdleme50trn2  39087  cdleme  39096  cdlemg2idN  39132  cdlemg7fvbwN  39143  cdlemg10bALTN  39172  cdlemg10a  39176  cdlemg12d  39182  cdlemg12g  39185  cdlemg12  39186  cdlemg13a  39187  cdlemg13  39188  cdlemg17b  39198  cdlemg17dN  39199  cdlemg17dALTN  39200  cdlemg17e  39201  cdlemg17f  39202  cdlemg17i  39205  cdlemg17pq  39208  cdlemg17bq  39209  cdlemg17iqN  39210  cdlemg18d  39217  cdlemg18  39218  cdlemg19a  39219  cdlemg19  39220  cdlemg21  39222  cdlemg27a  39228  cdlemg28a  39229  cdlemg31b0N  39230  cdlemg27b  39232  cdlemg31c  39235  cdlemg33b0  39237  cdlemg33c0  39238  cdlemg28  39240  cdlemg33a  39242  cdlemg33  39247  cdlemg36  39250  ltrnco  39255  cdlemg44  39269  cdlemg47  39272  tendococl  39308  tendoplcl  39317  cdlemh1  39351  cdlemh2  39352  cdlemh  39353  cdlemi  39356  tendocan  39360  cdlemk5  39372  cdlemk6  39373  cdlemk7  39384  cdlemk11  39385  cdlemk12  39386  cdlemkole  39389  cdlemk14  39390  cdlemk15  39391  cdlemk16a  39392  cdlemk16  39393  cdlemk18  39404  cdlemk19  39405  cdlemk7u  39406  cdlemk11u  39407  cdlemk12u  39408  cdlemk21N  39409  cdlemk20  39410  cdlemkoatnle-2N  39411  cdlemk13-2N  39412  cdlemkole-2N  39413  cdlemk14-2N  39414  cdlemk15-2N  39415  cdlemk16-2N  39416  cdlemk17-2N  39417  cdlemk18-2N  39422  cdlemk19-2N  39423  cdlemk7u-2N  39424  cdlemk11u-2N  39425  cdlemk12u-2N  39426  cdlemk21-2N  39427  cdlemk20-2N  39428  cdlemk22  39429  cdlemk27-3  39443  cdlemk33N  39445  cdlemk11ta  39465  cdlemkid3N  39469  cdlemk11tc  39481  cdlemk11t  39482  cdlemk45  39483  cdlemk46  39484  cdlemk47  39485  cdlemk48  39486  cdlemk49  39487  cdlemk50  39488  cdlemk51  39489  cdlemk52  39490  cdlemk53a  39491  cdlemk55b  39496  cdlemkyyN  39498  cdlemk55u1  39501  cdlemk39u1  39503  cdlemk56  39507  cdlemm10N  39654  dihord1  39754  dihord2a  39755  dihord2b  39756  dihord10  39759  dihord4  39794  dihord5apre  39798  dihglblem2N  39830  dihjatc1  39847  dihjatc2N  39848  dihjatc3  39849  dihmeetlem15N  39857  dihmeetlem20N  39862  mapdpglem24  40240  hdmap14lem11  40414  hdmap14lem12  40415  flt4lem5  41046  mzpsubst  41129  monotuz  41323  congmul  41349  congsub  41352  ntrclsiso  42461  ntrclskb  42463  ntrclsk3  42464  infleinf  43727  mullimc  43977  mullimcf  43984  0ellimcdiv  44010  limclner  44012  sge0xaddlem2  44795  lincdifsn  46625  itschlc0yqe  46966  itscnhlc0xyqsol  46971  itsclc0xyqsolr  46975  itsclquadeu  46983