Theorem simp13 1201

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  simp113  1300  simp213  1309  simp313  1318  omeu  8211  ackbij1lem16  9657  dvdsgcd  15892  coprimeprodsq  16145  pythagtriplem4  16156  pythagtriplem13  16164  pythagtriplem14  16165  pythagtriplem16  16167  pythagtrip  16171  lsmpropd  18803  matsc  21059  mdetunilem7  21227  smadiadetglem2  21281  m2cpminvid  21361  pmatcollpw1lem1  21382  mp2pm2mplem2  21415  isfil2  22464  filuni  22493  ufprim  22517  cxple2a  25282  isosctr  25399  brbtwn2  26691  colinearalg  26696  ax5seg  26724  axcontlem4  26753  measres  31481  bayesth  31697  nolesgn2o  33178  ofscom  33468  btwndiff  33488  ifscgr  33505  brofs2  33538  brifs2  33539  fscgr  33541  btwnconn1lem1  33548  btwnconn1lem2  33549  btwnconn1lem3  33550  btwnconn1lem4  33551  btwnconn1lem12  33559  seglecgr12im  33571  seglecgr12  33572  ivthALT  33683  islshpcv  36204  eqlkr  36250  lshpsmreu  36260  lshpkrlem5  36265  atlrelat1  36472  cvlcvr1  36490  cvlcvrp  36491  cvlatcvr1  36492  cvlatcvr2  36493  4noncolr3  36604  4noncolr2  36605  4noncolr1  36606  athgt  36607  3dimlem2  36610  3dimlem3a  36611  3dimlem4a  36614  3dimlem4  36615  3dimlem4OLDN  36616  3dim1  36618  3dim2  36619  hlatexch4  36632  ps-2b  36633  3atlem6  36639  llnnleat  36664  2atm  36678  ps-2c  36679  llnmlplnN  36690  2atmat  36712  2llnjN  36718  lvoli2  36732  4atlem3b  36749  4atlem10  36757  4atlem11a  36758  4atlem11b  36759  4atlem12a  36761  4atlem12b  36762  dalemswapyz  36807  lneq2at  36929  2lnat  36935  cdlema1N  36942  cdlemb  36945  pmodlem1  36997  llnmod2i2  37014  dalawlem1  37022  dalawlem3  37024  dalawlem4  37025  dalawlem6  37027  dalawlem9  37030  dalawlem10  37031  dalawlem11  37032  dalawlem12  37033  dalawlem13  37034  dalawlem15  37036  dalaw  37037  pclfinN  37051  osumcllem5N  37111  osumcllem6N  37112  osumcllem7N  37113  osumcllem9N  37115  osumcllem11N  37117  pl42lem1N  37130  lhp2at0  37183  lhp2atne  37185  lhp2at0ne  37187  4atexlem7  37226  ldilco  37267  ltrneq  37300  cdlemd2  37350  cdleme0ex2N  37375  cdleme7aa  37393  cdleme7c  37396  cdleme7d  37397  cdleme7ga  37399  cdleme11c  37412  cdleme11l  37420  cdleme11  37421  cdleme14  37424  cdleme15a  37425  cdleme15c  37427  cdleme16b  37430  cdleme16c  37431  cdleme16d  37432  cdleme16e  37433  cdleme16f  37434  cdleme0nex  37441  cdleme19b  37455  cdleme19d  37457  cdleme19e  37458  cdleme20f  37465  cdleme20k  37470  cdleme20l1  37471  cdleme20l2  37472  cdleme20l  37473  cdleme20m  37474  cdleme21a  37476  cdleme21b  37477  cdleme21c  37478  cdleme21ct  37480  cdleme21d  37481  cdleme21e  37482  cdleme21f  37483  cdleme21i  37486  cdleme22cN  37493  cdleme22eALTN  37496  cdleme25a  37504  cdleme25c  37506  cdleme25dN  37507  cdleme26e  37510  cdleme26ee  37511  cdleme26eALTN  37512  cdleme26f2ALTN  37515  cdleme26f2  37516  cdleme28a  37521  cdleme28b  37522  cdleme28  37524  cdlemefr32sn2aw  37555  cdlemefs32sn1aw  37565  cdleme43fsv1snlem  37571  cdleme41sn3a  37584  cdleme32c  37594  cdleme32e  37596  cdleme32le  37598  cdleme35a  37599  cdleme35b  37601  cdleme35d  37603  cdleme36a  37611  cdleme36m  37612  cdleme39a  37616  cdleme40m  37618  cdleme40n  37619  cdleme43bN  37641  cdleme43dN  37643  cdleme46f2g2  37644  cdleme46f2g1  37645  cdleme4gfv  37658  cdlemeg49le  37662  cdlemeg46c  37664  cdlemeg46fvaw  37667  cdlemeg46nlpq  37668  cdlemeg46gfre  37683  cdleme50trn2  37702  cdlemg2ce  37743  cdlemg2idN  37747  cdlemg7fvbwN  37758  cdlemg10bALTN  37787  cdlemg10a  37791  cdlemg12d  37797  cdlemg12g  37800  cdlemg12  37801  cdlemg13a  37802  cdlemg13  37803  cdlemg17b  37813  cdlemg17dN  37814  cdlemg17dALTN  37815  cdlemg17e  37816  cdlemg17pq  37823  cdlemg17bq  37824  cdlemg18d  37832  cdlemg19a  37834  cdlemg19  37835  cdlemg21  37837  cdlemg27a  37843  cdlemg31b0N  37845  cdlemg27b  37847  cdlemg31c  37850  cdlemg33b0  37852  cdlemg33c0  37853  cdlemg28b  37854  cdlemg33a  37857  cdlemg33  37862  ltrnco  37870  cdlemg44  37884  cdlemg47  37887  tendococl  37923  tendoplcl  37932  cdlemh1  37966  cdlemh2  37967  cdlemh  37968  cdlemi  37971  cdlemk5  37987  cdlemk6  37988  cdlemksel  37996  cdlemksv2  37998  cdlemk7  37999  cdlemk11  38000  cdlemk12  38001  cdlemkole  38004  cdlemk14  38005  cdlemk15  38006  cdlemk16a  38007  cdlemk16  38008  cdlemk1u  38010  cdlemk5u  38012  cdlemk6u  38013  cdlemkuel  38016  cdlemkuv2  38018  cdlemk18  38019  cdlemk19  38020  cdlemk7u  38021  cdlemk11u  38022  cdlemk12u  38023  cdlemk21N  38024  cdlemk20  38025  cdlemkoatnle-2N  38026  cdlemk13-2N  38027  cdlemkole-2N  38028  cdlemk14-2N  38029  cdlemk15-2N  38030  cdlemk16-2N  38031  cdlemk17-2N  38032  cdlemk18-2N  38037  cdlemk19-2N  38038  cdlemk7u-2N  38039  cdlemk11u-2N  38040  cdlemk12u-2N  38041  cdlemk21-2N  38042  cdlemk20-2N  38043  cdlemkuel-3  38049  cdlemkuv2-3N  38050  cdlemk22-3  38052  cdlemk33N  38060  cdlemk47  38100  cdlemk48  38101  cdlemk49  38102  cdlemk50  38103  cdlemk51  38104  cdlemk52  38105  cdlemk53a  38106  cdlemk55b  38111  cdlemkyyN  38113  cdlemk55u1  38116  cdlemk39u1  38118  cdlemk56  38122  dihord1  38369  dihord2a  38370  dihord10  38374  dihord11c  38375  dihord4  38409  dihord5apre  38413  dihglblem2N  38445  dihglbcpreN  38451  dihmeetlem3N  38456  dihjatc1  38462  dihjatc2N  38463  dihjatc3  38464  mapdpglem24  38855  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  hdmap14lem11  39029  hdmap14lem12  39030  hdmapglem7  39080  mzpsubst  39365  congmul  39584  congsub  39587  ntrclsiso  40437  ntrclskb  40439  ntrclsk3  40440  limsupre  41942  0ellimcdiv  41950  limclner  41952  sge0xaddlem2  42736  lincdifsn  44499  itschlc0yqe  44767  itscnhlc0xyqsol  44772