Theorem simp31 1208

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

Assertion

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

Proof of Theorem simp31

Step	Hyp	Ref	Expression
1		simp1 1135	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜒)
2	1	3ad2ant3 1134	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp131  1307  simp231  1316  simp331  1325  smogt  8207  frlmphl  20997  mdetuni0  21779  mdetmul  21781  gsummatr01lem3  21815  decpmatmullem  21929  tsmsxp  23315  log2sumbnd  26701  ax5seg  27315  wlkoniswlk  28038  iocinioc2  31109  totprob  32403  eqfunresadj  33744  nosupres  33919  noinfres  33934  cgrtr  34303  cgrtr3  34305  ofscom  34318  cgrextend  34319  segconeq  34321  ifscgr  34355  btwnxfr  34367  colinearxfr  34386  brofs2  34388  brifs2  34389  fscgr  34391  btwnconn1lem1  34398  btwnconn1lem2  34399  btwnconn1lem5  34402  btwnconn1lem6  34403  btwnconn1lem7  34404  btwnconn1lem8  34405  btwnconn1lem9  34406  btwnconn1lem10  34407  btwnconn1lem11  34408  btwnconn1lem12  34409  seglecgr12im  34421  seglecgr12  34422  segletr  34425  outsideofeq  34441  ivthALT  34533  lshpkrlem5  37135  lshpkrlem6  37136  exatleN  37425  atbtwn  37467  atbtwnexOLDN  37468  atbtwnex  37469  4noncolr3  37474  3dimlem3a  37481  3dimlem4a  37484  3dim1  37488  3dim2  37489  1cvrat  37497  2atjlej  37500  hlatexch4  37502  ps-2b  37503  2atm  37548  2atmat  37582  4atlem11b  37629  4atlem11  37630  4at  37634  4at2  37635  2lplnja  37640  2lplnj  37641  dalemswapyz  37677  dalemccnedd  37708  cdlemb  37815  paddasslem5  37845  paddasslem15  37855  pmodlem1  37867  dalawlem1  37892  dalawlem3  37894  dalawlem4  37895  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem9  37900  dalawlem11  37902  dalawlem12  37903  dalawlem15  37906  osumcllem5N  37981  osumcllem6N  37982  lhpexle3lem  38032  lhpmcvr4N  38047  lhpmcvr6N  38049  4atex2  38098  4atex2-0bOLDN  38100  4atex3  38102  ltrn11at  38168  trlval3  38208  cdlemd3  38221  cdleme0moN  38246  cdleme7aa  38263  cdleme7b  38265  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme7  38270  cdleme16aN  38280  cdleme11dN  38283  cdleme11e  38284  cdleme11l  38290  cdleme11  38291  cdleme12  38292  cdleme14  38294  cdleme15b  38296  cdleme15c  38297  cdleme16b  38300  cdleme16c  38301  cdleme16d  38302  cdleme16e  38303  cdleme16f  38304  cdleme17c  38309  cdleme18c  38314  cdleme18d  38316  cdlemeda  38319  cdleme19a  38324  cdleme19b  38325  cdleme19c  38326  cdleme20aN  38330  cdleme20bN  38331  cdleme20d  38333  cdleme20i  38338  cdleme20j  38339  cdleme20l1  38341  cdleme20l2  38342  cdleme21d  38351  cdleme21e  38352  cdleme21f  38353  cdleme22aa  38360  cdleme22e  38365  cdleme22eALTN  38366  cdleme22f2  38368  cdleme22g  38369  cdleme23b  38371  cdleme26eALTN  38382  cdleme26fALTN  38383  cdleme26f  38384  cdleme26f2ALTN  38385  cdleme26f2  38386  cdleme28a  38391  cdleme28b  38392  cdleme32b  38463  cdleme32c  38464  cdleme32e  38466  cdleme35h  38477  cdleme35sn2aw  38479  cdleme41sn3aw  38495  cdleme41sn4aw  38496  cdlemeg46gfre  38553  cdlemf1  38582  cdlemg1cex  38609  cdlemg2ce  38613  cdlemg4d  38634  cdlemg4e  38635  cdlemg4f  38636  cdlemg4  38638  cdlemg6d  38642  cdlemg6e  38643  cdlemg7fvN  38645  cdlemg8b  38649  cdlemg8c  38650  cdlemg9a  38653  cdlemg9b  38654  cdlemg9  38655  cdlemg11aq  38659  cdlemg10a  38661  cdlemg12a  38664  cdlemg12b  38665  cdlemg12c  38666  cdlemg12d  38667  cdlemg13  38673  cdlemg14f  38674  cdlemg14g  38675  cdlemg17b  38683  cdlemg17dN  38684  cdlemg17e  38686  cdlemg17i  38690  cdlemg17pq  38693  cdlemg17iqN  38695  cdlemg18c  38701  cdlemg18d  38702  cdlemg18  38703  cdlemg19  38705  cdlemg21  38707  cdlemg27a  38713  cdlemg31b0N  38715  cdlemg27b  38717  cdlemg31c  38720  cdlemg33b0  38722  cdlemg33c0  38723  cdlemg33  38732  cdlemg35  38734  cdlemg43  38751  cdlemg44a  38752  cdlemg46  38756  cdlemh2  38837  cdlemh  38838  cdlemj1  38842  cdlemk3  38854  cdlemk5  38857  cdlemk6  38858  cdlemki  38862  cdlemksv2  38868  cdlemk12  38871  cdlemk15  38876  cdlemk16  38878  cdlemk18  38889  cdlemk19  38890  cdlemk7u  38891  cdlemk12u  38893  cdlemkoatnle-2N  38896  cdlemk13-2N  38897  cdlemkole-2N  38898  cdlemk14-2N  38899  cdlemk15-2N  38900  cdlemk16-2N  38901  cdlemk17-2N  38902  cdlemk18-2N  38907  cdlemk19-2N  38908  cdlemk7u-2N  38909  cdlemk11u-2N  38910  cdlemk12u-2N  38911  cdlemk20-2N  38913  cdlemk22  38914  cdlemk30  38915  cdlemk31  38917  cdlemk24-3  38924  cdlemkid2  38945  cdlemkfid3N  38946  cdlemk11ta  38950  cdlemkid3N  38954  cdlemk11tc  38966  cdlemk45  38968  cdlemk46  38969  cdlemk47  38970  cdlemk52  38975  cdlemk53a  38976  cdlemk53b  38977  cdleml1N  38997  cdleml3N  38999  cdlemn7  39224  cdlemn10  39227  dihordlem7  39235  dihord1  39239  dihord11c  39245  dihord2  39248  hlhilphllem  39984  fmuldfeq  43131  seposep  46230  iscnrm3rlem8  46252  iscnrm3llem2  46255