Theorem simp13 1207

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

Assertion

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

Proof of Theorem simp13

Step	Hyp	Ref	Expression
1		simp3 1139	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant1 1134	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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simp113  1306  simp213  1315  simp313  1324  omeu  8522  ackbij1lem16  10156  dvdsgcd  16483  coprimeprodsq  16748  pythagtriplem4  16759  pythagtriplem13  16767  pythagtriplem14  16768  pythagtriplem16  16770  pythagtrip  16774  lsmpropd  19618  matsc  22406  mdetunilem7  22574  smadiadetglem2  22628  m2cpminvid  22709  pmatcollpw1lem1  22730  mp2pm2mplem2  22763  isfil2  23812  filuni  23841  ufprim  23865  cxple2a  26676  isosctr  26799  nolesgn2o  27651  nogesgn1o  27653  sltstr  27795  cofcut2  27930  onsfi  28364  brbtwn2  28990  colinearalg  28995  ax5seg  29023  axcontlem4  29052  measres  34399  bayesth  34616  ofscom  36220  btwndiff  36240  ifscgr  36257  brofs2  36290  brifs2  36291  fscgr  36293  btwnconn1lem1  36300  btwnconn1lem2  36301  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem12  36311  seglecgr12im  36323  seglecgr12  36324  ivthALT  36548  islshpcv  39426  eqlkr  39472  lshpsmreu  39482  lshpkrlem5  39487  atlrelat1  39694  cvlcvr1  39712  cvlcvrp  39713  cvlatcvr1  39714  cvlatcvr2  39715  4noncolr3  39826  4noncolr2  39827  4noncolr1  39828  athgt  39829  3dimlem2  39832  3dimlem3a  39833  3dimlem4a  39836  3dimlem4  39837  3dimlem4OLDN  39838  3dim1  39840  3dim2  39841  hlatexch4  39854  ps-2b  39855  3atlem6  39861  llnnleat  39886  2atm  39900  ps-2c  39901  llnmlplnN  39912  2atmat  39934  2llnjN  39940  lvoli2  39954  4atlem3b  39971  4atlem10  39979  4atlem11a  39980  4atlem11b  39981  4atlem12a  39983  4atlem12b  39984  dalemswapyz  40029  lneq2at  40151  2lnat  40157  cdlema1N  40164  cdlemb  40167  pmodlem1  40219  llnmod2i2  40236  dalawlem1  40244  dalawlem3  40246  dalawlem4  40247  dalawlem6  40249  dalawlem9  40252  dalawlem10  40253  dalawlem11  40254  dalawlem12  40255  dalawlem13  40256  dalawlem15  40258  dalaw  40259  pclfinN  40273  osumcllem5N  40333  osumcllem6N  40334  osumcllem7N  40335  osumcllem9N  40337  osumcllem11N  40339  pl42lem1N  40352  lhp2at0  40405  lhp2atne  40407  lhp2at0ne  40409  4atexlem7  40448  ldilco  40489  ltrneq  40522  cdlemd2  40572  cdleme0ex2N  40597  cdleme7aa  40615  cdleme7c  40618  cdleme7d  40619  cdleme7ga  40621  cdleme11c  40634  cdleme11l  40642  cdleme11  40643  cdleme14  40646  cdleme15a  40647  cdleme15c  40649  cdleme16b  40652  cdleme16c  40653  cdleme16d  40654  cdleme16e  40655  cdleme16f  40656  cdleme0nex  40663  cdleme19b  40677  cdleme19d  40679  cdleme19e  40680  cdleme20f  40687  cdleme20k  40692  cdleme20l1  40693  cdleme20l2  40694  cdleme20l  40695  cdleme20m  40696  cdleme21a  40698  cdleme21b  40699  cdleme21c  40700  cdleme21ct  40702  cdleme21d  40703  cdleme21e  40704  cdleme21f  40705  cdleme21i  40708  cdleme22cN  40715  cdleme22eALTN  40718  cdleme25a  40726  cdleme25c  40728  cdleme25dN  40729  cdleme26e  40732  cdleme26ee  40733  cdleme26eALTN  40734  cdleme26f2ALTN  40737  cdleme26f2  40738  cdleme28a  40743  cdleme28b  40744  cdleme28  40746  cdlemefr32sn2aw  40777  cdlemefs32sn1aw  40787  cdleme43fsv1snlem  40793  cdleme41sn3a  40806  cdleme32c  40816  cdleme32e  40818  cdleme32le  40820  cdleme35a  40821  cdleme35b  40823  cdleme35d  40825  cdleme36a  40833  cdleme36m  40834  cdleme39a  40838  cdleme40m  40840  cdleme40n  40841  cdleme43bN  40863  cdleme43dN  40865  cdleme46f2g2  40866  cdleme46f2g1  40867  cdleme4gfv  40880  cdlemeg49le  40884  cdlemeg46c  40886  cdlemeg46fvaw  40889  cdlemeg46nlpq  40890  cdlemeg46gfre  40905  cdleme50trn2  40924  cdlemg2ce  40965  cdlemg2idN  40969  cdlemg7fvbwN  40980  cdlemg10bALTN  41009  cdlemg10a  41013  cdlemg12d  41019  cdlemg12g  41022  cdlemg12  41023  cdlemg13a  41024  cdlemg13  41025  cdlemg17b  41035  cdlemg17dN  41036  cdlemg17dALTN  41037  cdlemg17e  41038  cdlemg17pq  41045  cdlemg17bq  41046  cdlemg18d  41054  cdlemg19a  41056  cdlemg19  41057  cdlemg21  41059  cdlemg27a  41065  cdlemg31b0N  41067  cdlemg27b  41069  cdlemg31c  41072  cdlemg33b0  41074  cdlemg33c0  41075  cdlemg28b  41076  cdlemg33a  41079  cdlemg33  41084  ltrnco  41092  cdlemg44  41106  cdlemg47  41109  tendococl  41145  tendoplcl  41154  cdlemh1  41188  cdlemh2  41189  cdlemh  41190  cdlemi  41193  cdlemk5  41209  cdlemk6  41210  cdlemksel  41218  cdlemksv2  41220  cdlemk7  41221  cdlemk11  41222  cdlemk12  41223  cdlemkole  41226  cdlemk14  41227  cdlemk15  41228  cdlemk16a  41229  cdlemk16  41230  cdlemk1u  41232  cdlemk5u  41234  cdlemk6u  41235  cdlemkuel  41238  cdlemkuv2  41240  cdlemk18  41241  cdlemk19  41242  cdlemk7u  41243  cdlemk11u  41244  cdlemk12u  41245  cdlemk21N  41246  cdlemk20  41247  cdlemkoatnle-2N  41248  cdlemk13-2N  41249  cdlemkole-2N  41250  cdlemk14-2N  41251  cdlemk15-2N  41252  cdlemk16-2N  41253  cdlemk17-2N  41254  cdlemk18-2N  41259  cdlemk19-2N  41260  cdlemk7u-2N  41261  cdlemk11u-2N  41262  cdlemk12u-2N  41263  cdlemk21-2N  41264  cdlemk20-2N  41265  cdlemkuel-3  41271  cdlemkuv2-3N  41272  cdlemk22-3  41274  cdlemk33N  41282  cdlemk47  41322  cdlemk48  41323  cdlemk49  41324  cdlemk50  41325  cdlemk51  41326  cdlemk52  41327  cdlemk53a  41328  cdlemk55b  41333  cdlemkyyN  41335  cdlemk55u1  41338  cdlemk39u1  41340  cdlemk56  41344  dihord1  41591  dihord2a  41592  dihord10  41596  dihord11c  41597  dihord4  41631  dihord5apre  41635  dihglblem2N  41667  dihglbcpreN  41673  dihmeetlem3N  41678  dihjatc1  41684  dihjatc2N  41685  dihjatc3  41686  mapdpglem24  42077  baerlem3lem2  42083  baerlem5alem2  42084  baerlem5blem2  42085  hdmap14lem11  42251  hdmap14lem12  42252  hdmapglem7  42302  mzpsubst  43102  congmul  43321  congsub  43324  ntrclsiso  44420  ntrclskb  44422  ntrclsk3  44423  limsupre  45996  0ellimcdiv  46004  limclner  46006  sge0xaddlem2  46789  clnbgr3stgrgrlim  48376  gpgedgvtx1  48419  lincdifsn  48781  itschlc0yqe  49117  itscnhlc0xyqsol  49122