Theorem simp13 1206

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp113  1305  simp213  1314  simp313  1323  omeu  8595  ackbij1lem16  10246  dvdsgcd  16561  coprimeprodsq  16826  pythagtriplem4  16837  pythagtriplem13  16845  pythagtriplem14  16846  pythagtriplem16  16848  pythagtrip  16852  lsmpropd  19656  matsc  22386  mdetunilem7  22554  smadiadetglem2  22608  m2cpminvid  22689  pmatcollpw1lem1  22710  mp2pm2mplem2  22743  isfil2  23792  filuni  23821  ufprim  23845  cxple2a  26658  isosctr  26781  nolesgn2o  27633  nogesgn1o  27635  sslttr  27769  cofcut2  27873  brbtwn2  28830  colinearalg  28835  ax5seg  28863  axcontlem4  28892  measres  34199  bayesth  34417  ofscom  35971  btwndiff  35991  ifscgr  36008  brofs2  36041  brifs2  36042  fscgr  36044  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem12  36062  seglecgr12im  36074  seglecgr12  36075  ivthALT  36299  islshpcv  39017  eqlkr  39063  lshpsmreu  39073  lshpkrlem5  39078  atlrelat1  39285  cvlcvr1  39303  cvlcvrp  39304  cvlatcvr1  39305  cvlatcvr2  39306  4noncolr3  39418  4noncolr2  39419  4noncolr1  39420  athgt  39421  3dimlem2  39424  3dimlem3a  39425  3dimlem4a  39428  3dimlem4  39429  3dimlem4OLDN  39430  3dim1  39432  3dim2  39433  hlatexch4  39446  ps-2b  39447  3atlem6  39453  llnnleat  39478  2atm  39492  ps-2c  39493  llnmlplnN  39504  2atmat  39526  2llnjN  39532  lvoli2  39546  4atlem3b  39563  4atlem10  39571  4atlem11a  39572  4atlem11b  39573  4atlem12a  39575  4atlem12b  39576  dalemswapyz  39621  lneq2at  39743  2lnat  39749  cdlema1N  39756  cdlemb  39759  pmodlem1  39811  llnmod2i2  39828  dalawlem1  39836  dalawlem3  39838  dalawlem4  39839  dalawlem6  39841  dalawlem9  39844  dalawlem10  39845  dalawlem11  39846  dalawlem12  39847  dalawlem13  39848  dalawlem15  39850  dalaw  39851  pclfinN  39865  osumcllem5N  39925  osumcllem6N  39926  osumcllem7N  39927  osumcllem9N  39929  osumcllem11N  39931  pl42lem1N  39944  lhp2at0  39997  lhp2atne  39999  lhp2at0ne  40001  4atexlem7  40040  ldilco  40081  ltrneq  40114  cdlemd2  40164  cdleme0ex2N  40189  cdleme7aa  40207  cdleme7c  40210  cdleme7d  40211  cdleme7ga  40213  cdleme11c  40226  cdleme11l  40234  cdleme11  40235  cdleme14  40238  cdleme15a  40239  cdleme15c  40241  cdleme16b  40244  cdleme16c  40245  cdleme16d  40246  cdleme16e  40247  cdleme16f  40248  cdleme0nex  40255  cdleme19b  40269  cdleme19d  40271  cdleme19e  40272  cdleme20f  40279  cdleme20k  40284  cdleme20l1  40285  cdleme20l2  40286  cdleme20l  40287  cdleme20m  40288  cdleme21a  40290  cdleme21b  40291  cdleme21c  40292  cdleme21ct  40294  cdleme21d  40295  cdleme21e  40296  cdleme21f  40297  cdleme21i  40300  cdleme22cN  40307  cdleme22eALTN  40310  cdleme25a  40318  cdleme25c  40320  cdleme25dN  40321  cdleme26e  40324  cdleme26ee  40325  cdleme26eALTN  40326  cdleme26f2ALTN  40329  cdleme26f2  40330  cdleme28a  40335  cdleme28b  40336  cdleme28  40338  cdlemefr32sn2aw  40369  cdlemefs32sn1aw  40379  cdleme43fsv1snlem  40385  cdleme41sn3a  40398  cdleme32c  40408  cdleme32e  40410  cdleme32le  40412  cdleme35a  40413  cdleme35b  40415  cdleme35d  40417  cdleme36a  40425  cdleme36m  40426  cdleme39a  40430  cdleme40m  40432  cdleme40n  40433  cdleme43bN  40455  cdleme43dN  40457  cdleme46f2g2  40458  cdleme46f2g1  40459  cdleme4gfv  40472  cdlemeg49le  40476  cdlemeg46c  40478  cdlemeg46fvaw  40481  cdlemeg46nlpq  40482  cdlemeg46gfre  40497  cdleme50trn2  40516  cdlemg2ce  40557  cdlemg2idN  40561  cdlemg7fvbwN  40572  cdlemg10bALTN  40601  cdlemg10a  40605  cdlemg12d  40611  cdlemg12g  40614  cdlemg12  40615  cdlemg13a  40616  cdlemg13  40617  cdlemg17b  40627  cdlemg17dN  40628  cdlemg17dALTN  40629  cdlemg17e  40630  cdlemg17pq  40637  cdlemg17bq  40638  cdlemg18d  40646  cdlemg19a  40648  cdlemg19  40649  cdlemg21  40651  cdlemg27a  40657  cdlemg31b0N  40659  cdlemg27b  40661  cdlemg31c  40664  cdlemg33b0  40666  cdlemg33c0  40667  cdlemg28b  40668  cdlemg33a  40671  cdlemg33  40676  ltrnco  40684  cdlemg44  40698  cdlemg47  40701  tendococl  40737  tendoplcl  40746  cdlemh1  40780  cdlemh2  40781  cdlemh  40782  cdlemi  40785  cdlemk5  40801  cdlemk6  40802  cdlemksel  40810  cdlemksv2  40812  cdlemk7  40813  cdlemk11  40814  cdlemk12  40815  cdlemkole  40818  cdlemk14  40819  cdlemk15  40820  cdlemk16a  40821  cdlemk16  40822  cdlemk1u  40824  cdlemk5u  40826  cdlemk6u  40827  cdlemkuel  40830  cdlemkuv2  40832  cdlemk18  40833  cdlemk19  40834  cdlemk7u  40835  cdlemk11u  40836  cdlemk12u  40837  cdlemk21N  40838  cdlemk20  40839  cdlemkoatnle-2N  40840  cdlemk13-2N  40841  cdlemkole-2N  40842  cdlemk14-2N  40843  cdlemk15-2N  40844  cdlemk16-2N  40845  cdlemk17-2N  40846  cdlemk18-2N  40851  cdlemk19-2N  40852  cdlemk7u-2N  40853  cdlemk11u-2N  40854  cdlemk12u-2N  40855  cdlemk21-2N  40856  cdlemk20-2N  40857  cdlemkuel-3  40863  cdlemkuv2-3N  40864  cdlemk22-3  40866  cdlemk33N  40874  cdlemk47  40914  cdlemk48  40915  cdlemk49  40916  cdlemk50  40917  cdlemk51  40918  cdlemk52  40919  cdlemk53a  40920  cdlemk55b  40925  cdlemkyyN  40927  cdlemk55u1  40930  cdlemk39u1  40932  cdlemk56  40936  dihord1  41183  dihord2a  41184  dihord10  41188  dihord11c  41189  dihord4  41223  dihord5apre  41227  dihglblem2N  41259  dihglbcpreN  41265  dihmeetlem3N  41270  dihjatc1  41276  dihjatc2N  41277  dihjatc3  41278  mapdpglem24  41669  baerlem3lem2  41675  baerlem5alem2  41676  baerlem5blem2  41677  hdmap14lem11  41843  hdmap14lem12  41844  hdmapglem7  41894  mzpsubst  42718  congmul  42938  congsub  42941  ntrclsiso  44038  ntrclskb  44040  ntrclsk3  44041  limsupre  45618  0ellimcdiv  45626  limclner  45628  sge0xaddlem2  46411  gpgedgvtx1  48014  lincdifsn  48348  itschlc0yqe  48688  itscnhlc0xyqsol  48693