Theorem simp31 1207

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  simp131  1306  simp231  1315  simp331  1324  smogt  8169  frlmphl  20898  mdetuni0  21678  mdetmul  21680  gsummatr01lem3  21714  decpmatmullem  21828  tsmsxp  23214  log2sumbnd  26597  ax5seg  27209  wlkoniswlk  27931  iocinioc2  31002  totprob  32294  eqfunresadj  33641  nosupres  33837  noinfres  33852  cgrtr  34221  cgrtr3  34223  ofscom  34236  cgrextend  34237  segconeq  34239  ifscgr  34273  btwnxfr  34285  colinearxfr  34304  brofs2  34306  brifs2  34307  fscgr  34309  btwnconn1lem1  34316  btwnconn1lem2  34317  btwnconn1lem5  34320  btwnconn1lem6  34321  btwnconn1lem7  34322  btwnconn1lem8  34323  btwnconn1lem9  34324  btwnconn1lem10  34325  btwnconn1lem11  34326  btwnconn1lem12  34327  seglecgr12im  34339  seglecgr12  34340  segletr  34343  outsideofeq  34359  ivthALT  34451  lshpkrlem5  37055  lshpkrlem6  37056  exatleN  37345  atbtwn  37387  atbtwnexOLDN  37388  atbtwnex  37389  4noncolr3  37394  3dimlem3a  37401  3dimlem4a  37404  3dim1  37408  3dim2  37409  1cvrat  37417  2atjlej  37420  hlatexch4  37422  ps-2b  37423  2atm  37468  2atmat  37502  4atlem11b  37549  4atlem11  37550  4at  37554  4at2  37555  2lplnja  37560  2lplnj  37561  dalemswapyz  37597  dalemccnedd  37628  cdlemb  37735  paddasslem5  37765  paddasslem15  37775  pmodlem1  37787  dalawlem1  37812  dalawlem3  37814  dalawlem4  37815  dalawlem5  37816  dalawlem6  37817  dalawlem7  37818  dalawlem8  37819  dalawlem9  37820  dalawlem11  37822  dalawlem12  37823  dalawlem15  37826  osumcllem5N  37901  osumcllem6N  37902  lhpexle3lem  37952  lhpmcvr4N  37967  lhpmcvr6N  37969  4atex2  38018  4atex2-0bOLDN  38020  4atex3  38022  ltrn11at  38088  trlval3  38128  cdlemd3  38141  cdleme0moN  38166  cdleme7aa  38183  cdleme7b  38185  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme16aN  38200  cdleme11dN  38203  cdleme11e  38204  cdleme11l  38210  cdleme11  38211  cdleme12  38212  cdleme14  38214  cdleme15b  38216  cdleme15c  38217  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme16e  38223  cdleme16f  38224  cdleme17c  38229  cdleme18c  38234  cdleme18d  38236  cdlemeda  38239  cdleme19a  38244  cdleme19b  38245  cdleme19c  38246  cdleme20aN  38250  cdleme20bN  38251  cdleme20d  38253  cdleme20i  38258  cdleme20j  38259  cdleme20l1  38261  cdleme20l2  38262  cdleme21d  38271  cdleme21e  38272  cdleme21f  38273  cdleme22aa  38280  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f2  38288  cdleme22g  38289  cdleme23b  38291  cdleme26eALTN  38302  cdleme26fALTN  38303  cdleme26f  38304  cdleme26f2ALTN  38305  cdleme26f2  38306  cdleme28a  38311  cdleme28b  38312  cdleme32b  38383  cdleme32c  38384  cdleme32e  38386  cdleme35h  38397  cdleme35sn2aw  38399  cdleme41sn3aw  38415  cdleme41sn4aw  38416  cdlemeg46gfre  38473  cdlemf1  38502  cdlemg1cex  38529  cdlemg2ce  38533  cdlemg4d  38554  cdlemg4e  38555  cdlemg4f  38556  cdlemg4  38558  cdlemg6d  38562  cdlemg6e  38563  cdlemg7fvN  38565  cdlemg8b  38569  cdlemg8c  38570  cdlemg9a  38573  cdlemg9b  38574  cdlemg9  38575  cdlemg11aq  38579  cdlemg10a  38581  cdlemg12a  38584  cdlemg12b  38585  cdlemg12c  38586  cdlemg12d  38587  cdlemg13  38593  cdlemg14f  38594  cdlemg14g  38595  cdlemg17b  38603  cdlemg17dN  38604  cdlemg17e  38606  cdlemg17i  38610  cdlemg17pq  38613  cdlemg17iqN  38615  cdlemg18c  38621  cdlemg18d  38622  cdlemg18  38623  cdlemg19  38625  cdlemg21  38627  cdlemg27a  38633  cdlemg31b0N  38635  cdlemg27b  38637  cdlemg31c  38640  cdlemg33b0  38642  cdlemg33c0  38643  cdlemg33  38652  cdlemg35  38654  cdlemg43  38671  cdlemg44a  38672  cdlemg46  38676  cdlemh2  38757  cdlemh  38758  cdlemj1  38762  cdlemk3  38774  cdlemk5  38777  cdlemk6  38778  cdlemki  38782  cdlemksv2  38788  cdlemk12  38791  cdlemk15  38796  cdlemk16  38798  cdlemk18  38809  cdlemk19  38810  cdlemk7u  38811  cdlemk12u  38813  cdlemkoatnle-2N  38816  cdlemk13-2N  38817  cdlemkole-2N  38818  cdlemk14-2N  38819  cdlemk15-2N  38820  cdlemk16-2N  38821  cdlemk17-2N  38822  cdlemk18-2N  38827  cdlemk19-2N  38828  cdlemk7u-2N  38829  cdlemk11u-2N  38830  cdlemk12u-2N  38831  cdlemk20-2N  38833  cdlemk22  38834  cdlemk30  38835  cdlemk31  38837  cdlemk24-3  38844  cdlemkid2  38865  cdlemkfid3N  38866  cdlemk11ta  38870  cdlemkid3N  38874  cdlemk11tc  38886  cdlemk45  38888  cdlemk46  38889  cdlemk47  38890  cdlemk52  38895  cdlemk53a  38896  cdlemk53b  38897  cdleml1N  38917  cdleml3N  38919  cdlemn7  39144  cdlemn10  39147  dihordlem7  39155  dihord1  39159  dihord11c  39165  dihord2  39168  hlhilphllem  39904  fmuldfeq  43014  seposep  46107  iscnrm3rlem8  46129  iscnrm3llem2  46132