Theorem simp33 1099

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

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl33  1144  simpr33  1153  simp133  1198  simp233  1207  simp333  1216  smogt  7464  bitsfzo  15157  frlmphl  20120  mdetunilem4  20421  mdetuni0  20427  mdetmul  20429  decpmatmullem  20576  logexprlim  24950  ax5seg  25818  iocinioc2  29541  bnj966  31014  eqfunresadj  31659  cgrtr  32099  cgrtr3  32101  ofscom  32114  segconeq  32117  btwnxfr  32163  colinearxfr  32182  fscgr  32187  btwnconn1lem1  32194  btwnconn1lem2  32195  btwnconn1lem5  32198  btwnconn1lem6  32199  btwnconn1lem8  32201  btwnconn1lem9  32202  btwnconn1lem10  32203  btwnconn1lem11  32204  btwnconn1lem12  32205  brsegle2  32216  seglecgr12im  32217  seglecgr12  32218  segletr  32221  outsideofeq  32237  lshpkrlem5  34401  lshpkrlem6  34402  atbtwnexOLDN  34733  atbtwnex  34734  4noncolr3  34739  3dimlem3a  34746  3dimlem4a  34749  3dim1  34753  3dim2  34754  1cvrat  34762  2atjlej  34765  hlatexch4  34767  ps-2b  34768  2atm  34813  ps-2c  34814  lvolex3N  34824  2atmat  34847  lvolnlelpln  34871  4atlem10  34892  4atlem11b  34894  4atlem11  34895  4at  34899  4at2  34900  2lplnja  34905  2lplnj  34906  dalemclccjdd  34974  paddasslem5  35110  paddasslem15  35120  pmodlem1  35132  dalawlem1  35157  dalawlem3  35159  dalawlem4  35160  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  dalawlem15  35171  osumcllem5N  35246  osumcllem6N  35247  lhpexle3lem  35297  lhpmcvr4N  35312  lhpmcvr6N  35314  4atexlemex6  35360  4atex2  35363  4atex2-0bOLDN  35365  4atex3  35367  ltrn11at  35433  cdlemd3  35487  cdleme7aa  35529  cdleme7b  35531  cdleme7c  35532  cdleme7d  35533  cdleme7ga  35535  cdleme16aN  35546  cdleme11dN  35549  cdleme11e  35550  cdleme11l  35556  cdleme11  35557  cdleme12  35558  cdleme14  35560  cdleme15c  35563  cdleme16b  35566  cdleme16d  35568  cdleme17b  35574  cdleme17c  35575  cdleme18c  35580  cdleme18d  35582  cdlemeda  35585  cdlemednpq  35586  cdleme19a  35591  cdleme19c  35593  cdleme20aN  35597  cdleme20bN  35598  cdleme20d  35600  cdleme20f  35602  cdleme20g  35603  cdleme20j  35606  cdleme20l1  35608  cdleme21f  35620  cdleme22aa  35627  cdleme22a  35628  cdleme22cN  35630  cdleme22e  35632  cdleme22f2  35635  cdleme22g  35636  cdleme23b  35638  cdleme23c  35639  cdleme26e  35647  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme28a  35658  cdleme28b  35659  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme35h2  35745  cdleme38m  35751  cdleme41sn4aw  35763  cdlemf1  35849  cdlemg1cex  35876  cdlemg2ce  35880  cdlemg4d  35901  cdlemg4f  35903  cdlemg7fvN  35912  cdlemg8a  35915  cdlemg8b  35916  cdlemg8c  35917  cdlemg9a  35920  cdlemg11a  35925  cdlemg11aq  35926  cdlemg10a  35928  cdlemg11b  35930  cdlemg12a  35931  cdlemg12b  35932  cdlemg12d  35934  cdlemg12e  35935  cdlemg12f  35936  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg13  35940  cdlemg14f  35941  cdlemg14g  35942  cdlemg17b  35950  cdlemg17dN  35951  cdlemg17e  35953  cdlemg17h  35956  cdlemg17pq  35960  cdlemg17iqN  35962  cdlemg18b  35967  cdlemg18c  35968  cdlemg18d  35969  cdlemg18  35970  cdlemg19  35972  cdlemg21  35974  cdlemg27a  35980  cdlemg31b0N  35982  cdlemg27b  35984  cdlemg33b0  35989  cdlemg33c0  35990  cdlemg28  35992  cdlemg33a  35994  cdlemg35  36001  cdlemg42  36017  cdlemg44a  36019  cdlemg47  36024  cdlemh2  36104  cdlemh  36105  cdlemj1  36109  cdlemk3  36121  cdlemk5  36124  cdlemki  36129  cdlemksv2  36135  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemkole  36141  cdlemk14  36142  cdlemk15  36143  cdlemk16a  36144  cdlemk16  36145  cdlemkj  36151  cdlemkuv2  36155  cdlemk18  36156  cdlemk19  36157  cdlemk7u  36158  cdlemk12u  36160  cdlemkoatnle-2N  36163  cdlemk13-2N  36164  cdlemkole-2N  36165  cdlemk14-2N  36166  cdlemk15-2N  36167  cdlemk16-2N  36168  cdlemk17-2N  36169  cdlemk18-2N  36174  cdlemk19-2N  36175  cdlemk7u-2N  36176  cdlemk11u-2N  36177  cdlemk12u-2N  36178  cdlemk21-2N  36179  cdlemk20-2N  36180  cdlemk22  36181  cdlemk30  36182  cdlemk31  36184  cdlemk32  36185  cdlemk24-3  36191  cdlemkid2  36212  cdlemkfid3N  36213  cdlemk45  36235  cdlemk46  36236  cdlemk47  36237  cdlemk52  36242  cdlemk53a  36243  cdleml1N  36264  cdleml3N  36266  cdlemn7  36492  cdlemn10  36495  dihordlem7  36503  dihord1  36507  dihord2a  36508  dihord10  36512  dihord11c  36513  dihord2pre2  36515  hlhilphllem  37251  fmuldfeq  39815