Theorem simp33 1209

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

Assertion

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

Proof of Theorem simp33

Step	Hyp	Ref	Expression
1		simp3 1136	. 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:  simp133  1308  simp233  1317  simp333  1326  smogt  8169  bitsfzo  16070  frlmphl  20898  mdetunilem4  21672  mdetuni0  21678  mdetmul  21680  decpmatmullem  21828  logexprlim  26278  ax5seg  27209  iocinioc2  31002  bnj966  32824  eqfunresadj  33641  noinfres  33852  cgrtr  34221  cgrtr3  34223  ofscom  34236  segconeq  34239  btwnxfr  34285  colinearxfr  34304  fscgr  34309  btwnconn1lem1  34316  btwnconn1lem2  34317  btwnconn1lem5  34320  btwnconn1lem6  34321  btwnconn1lem8  34323  btwnconn1lem9  34324  btwnconn1lem10  34325  btwnconn1lem11  34326  btwnconn1lem12  34327  brsegle2  34338  seglecgr12im  34339  seglecgr12  34340  segletr  34343  outsideofeq  34359  lshpkrlem5  37055  lshpkrlem6  37056  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  ps-2c  37469  lvolex3N  37479  2atmat  37502  lvolnlelpln  37526  4atlem10  37547  4atlem11b  37549  4atlem11  37550  4at  37554  4at2  37555  2lplnja  37560  2lplnj  37561  dalemclccjdd  37629  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  4atexlemex6  38015  4atex2  38018  4atex2-0bOLDN  38020  4atex3  38022  ltrn11at  38088  cdlemd3  38141  cdleme7aa  38183  cdleme7b  38185  cdleme7c  38186  cdleme7d  38187  cdleme7ga  38189  cdleme16aN  38200  cdleme11dN  38203  cdleme11e  38204  cdleme11l  38210  cdleme11  38211  cdleme12  38212  cdleme14  38214  cdleme15c  38217  cdleme16b  38220  cdleme16d  38222  cdleme17b  38228  cdleme17c  38229  cdleme18c  38234  cdleme18d  38236  cdlemeda  38239  cdlemednpq  38240  cdleme19a  38244  cdleme19c  38246  cdleme20aN  38250  cdleme20bN  38251  cdleme20d  38253  cdleme20f  38255  cdleme20g  38256  cdleme20j  38259  cdleme20l1  38261  cdleme21f  38273  cdleme22aa  38280  cdleme22a  38281  cdleme22cN  38283  cdleme22e  38285  cdleme22f2  38288  cdleme22g  38289  cdleme23b  38291  cdleme23c  38292  cdleme26e  38300  cdleme26fALTN  38303  cdleme26f  38304  cdleme26f2ALTN  38305  cdleme26f2  38306  cdleme28a  38311  cdleme28b  38312  cdleme32b  38383  cdleme32c  38384  cdleme32e  38386  cdleme35h2  38398  cdleme38m  38404  cdleme41sn4aw  38416  cdlemf1  38502  cdlemg1cex  38529  cdlemg2ce  38533  cdlemg4d  38554  cdlemg4f  38556  cdlemg7fvN  38565  cdlemg8a  38568  cdlemg8b  38569  cdlemg8c  38570  cdlemg9a  38573  cdlemg11a  38578  cdlemg11aq  38579  cdlemg10a  38581  cdlemg11b  38583  cdlemg12a  38584  cdlemg12b  38585  cdlemg12d  38587  cdlemg12e  38588  cdlemg12f  38589  cdlemg12g  38590  cdlemg12  38591  cdlemg13a  38592  cdlemg13  38593  cdlemg14f  38594  cdlemg14g  38595  cdlemg17b  38603  cdlemg17dN  38604  cdlemg17e  38606  cdlemg17h  38609  cdlemg17pq  38613  cdlemg17iqN  38615  cdlemg18b  38620  cdlemg18c  38621  cdlemg18d  38622  cdlemg18  38623  cdlemg19  38625  cdlemg21  38627  cdlemg27a  38633  cdlemg31b0N  38635  cdlemg27b  38637  cdlemg33b0  38642  cdlemg33c0  38643  cdlemg28  38645  cdlemg33a  38647  cdlemg35  38654  cdlemg42  38670  cdlemg44a  38672  cdlemg47  38677  cdlemh2  38757  cdlemh  38758  cdlemj1  38762  cdlemk3  38774  cdlemk5  38777  cdlemki  38782  cdlemksv2  38788  cdlemk7  38789  cdlemk11  38790  cdlemk12  38791  cdlemkole  38794  cdlemk14  38795  cdlemk15  38796  cdlemk16a  38797  cdlemk16  38798  cdlemkj  38804  cdlemkuv2  38808  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  cdlemk21-2N  38832  cdlemk20-2N  38833  cdlemk22  38834  cdlemk30  38835  cdlemk31  38837  cdlemk32  38838  cdlemk24-3  38844  cdlemkid2  38865  cdlemkfid3N  38866  cdlemk45  38888  cdlemk46  38889  cdlemk47  38890  cdlemk52  38895  cdlemk53a  38896  cdleml1N  38917  cdleml3N  38919  cdlemn7  39144  cdlemn10  39147  dihordlem7  39155  dihord1  39159  dihord2a  39160  dihord10  39164  dihord11c  39165  dihord2pre2  39167  hlhilphllem  39904  fmuldfeq  43014  seposep  46107  iscnrm3rlem8  46129  iscnrm3llem2  46132