Theorem simp33 1212

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 1138	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜏)
2	1	3ad2ant3 1135	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp133  1311  simp233  1320  simp333  1329  eqfunresadj  7289  smogt  8282  bitsfzo  16341  frlmphl  21713  mdetunilem4  22525  mdetuni0  22531  mdetmul  22533  decpmatmullem  22681  logexprlim  27158  noinfres  27656  ax5seg  28911  iocinioc2  32754  bnj966  34948  cgrtr  36026  cgrtr3  36028  ofscom  36041  segconeq  36044  btwnxfr  36090  colinearxfr  36109  fscgr  36114  btwnconn1lem1  36121  btwnconn1lem2  36122  btwnconn1lem5  36125  btwnconn1lem6  36126  btwnconn1lem8  36128  btwnconn1lem9  36129  btwnconn1lem10  36130  btwnconn1lem11  36131  btwnconn1lem12  36132  brsegle2  36143  seglecgr12im  36144  seglecgr12  36145  segletr  36148  outsideofeq  36164  lshpkrlem5  39153  lshpkrlem6  39154  atbtwnexOLDN  39486  atbtwnex  39487  4noncolr3  39492  3dimlem3a  39499  3dimlem4a  39502  3dim1  39506  3dim2  39507  1cvrat  39515  2atjlej  39518  hlatexch4  39520  ps-2b  39521  2atm  39566  ps-2c  39567  lvolex3N  39577  2atmat  39600  lvolnlelpln  39624  4atlem10  39645  4atlem11b  39647  4atlem11  39648  4at  39652  4at2  39653  2lplnja  39658  2lplnj  39659  dalemclccjdd  39727  paddasslem5  39863  paddasslem15  39873  pmodlem1  39885  dalawlem1  39910  dalawlem3  39912  dalawlem4  39913  dalawlem5  39914  dalawlem6  39915  dalawlem7  39916  dalawlem8  39917  dalawlem9  39918  dalawlem11  39920  dalawlem12  39921  dalawlem15  39924  osumcllem5N  39999  osumcllem6N  40000  lhpexle3lem  40050  lhpmcvr4N  40065  lhpmcvr6N  40067  4atexlemex6  40113  4atex2  40116  4atex2-0bOLDN  40118  4atex3  40120  ltrn11at  40186  cdlemd3  40239  cdleme7aa  40281  cdleme7b  40283  cdleme7c  40284  cdleme7d  40285  cdleme7ga  40287  cdleme16aN  40298  cdleme11dN  40301  cdleme11e  40302  cdleme11l  40308  cdleme11  40309  cdleme12  40310  cdleme14  40312  cdleme15c  40315  cdleme16b  40318  cdleme16d  40320  cdleme17b  40326  cdleme17c  40327  cdleme18c  40332  cdleme18d  40334  cdlemeda  40337  cdlemednpq  40338  cdleme19a  40342  cdleme19c  40344  cdleme20aN  40348  cdleme20bN  40349  cdleme20d  40351  cdleme20f  40353  cdleme20g  40354  cdleme20j  40357  cdleme20l1  40359  cdleme21f  40371  cdleme22aa  40378  cdleme22a  40379  cdleme22cN  40381  cdleme22e  40383  cdleme22f2  40386  cdleme22g  40387  cdleme23b  40389  cdleme23c  40390  cdleme26e  40398  cdleme26fALTN  40401  cdleme26f  40402  cdleme26f2ALTN  40403  cdleme26f2  40404  cdleme28a  40409  cdleme28b  40410  cdleme32b  40481  cdleme32c  40482  cdleme32e  40484  cdleme35h2  40496  cdleme38m  40502  cdleme41sn4aw  40514  cdlemf1  40600  cdlemg1cex  40627  cdlemg2ce  40631  cdlemg4d  40652  cdlemg4f  40654  cdlemg7fvN  40663  cdlemg8a  40666  cdlemg8b  40667  cdlemg8c  40668  cdlemg9a  40671  cdlemg11a  40676  cdlemg11aq  40677  cdlemg10a  40679  cdlemg11b  40681  cdlemg12a  40682  cdlemg12b  40683  cdlemg12d  40685  cdlemg12e  40686  cdlemg12f  40687  cdlemg12g  40688  cdlemg12  40689  cdlemg13a  40690  cdlemg13  40691  cdlemg14f  40692  cdlemg14g  40693  cdlemg17b  40701  cdlemg17dN  40702  cdlemg17e  40704  cdlemg17h  40707  cdlemg17pq  40711  cdlemg17iqN  40713  cdlemg18b  40718  cdlemg18c  40719  cdlemg18d  40720  cdlemg18  40721  cdlemg19  40723  cdlemg21  40725  cdlemg27a  40731  cdlemg31b0N  40733  cdlemg27b  40735  cdlemg33b0  40740  cdlemg33c0  40741  cdlemg28  40743  cdlemg33a  40745  cdlemg35  40752  cdlemg42  40768  cdlemg44a  40770  cdlemg47  40775  cdlemh2  40855  cdlemh  40856  cdlemj1  40860  cdlemk3  40872  cdlemk5  40875  cdlemki  40880  cdlemksv2  40886  cdlemk7  40887  cdlemk11  40888  cdlemk12  40889  cdlemkole  40892  cdlemk14  40893  cdlemk15  40894  cdlemk16a  40895  cdlemk16  40896  cdlemkj  40902  cdlemkuv2  40906  cdlemk18  40907  cdlemk19  40908  cdlemk7u  40909  cdlemk12u  40911  cdlemkoatnle-2N  40914  cdlemk13-2N  40915  cdlemkole-2N  40916  cdlemk14-2N  40917  cdlemk15-2N  40918  cdlemk16-2N  40919  cdlemk17-2N  40920  cdlemk18-2N  40925  cdlemk19-2N  40926  cdlemk7u-2N  40927  cdlemk11u-2N  40928  cdlemk12u-2N  40929  cdlemk21-2N  40930  cdlemk20-2N  40931  cdlemk22  40932  cdlemk30  40933  cdlemk31  40935  cdlemk32  40936  cdlemk24-3  40942  cdlemkid2  40963  cdlemkfid3N  40964  cdlemk45  40986  cdlemk46  40987  cdlemk47  40988  cdlemk52  40993  cdlemk53a  40994  cdleml1N  41015  cdleml3N  41017  cdlemn7  41242  cdlemn10  41245  dihordlem7  41253  dihord1  41257  dihord2a  41258  dihord10  41262  dihord11c  41263  dihord2pre2  41265  hlhilphllem  41998  fmuldfeq  45623  usgrgrtrirex  47981  grlimprclnbgredg  48028  seposep  48957  iscnrm3rlem8  48978  iscnrm3llem2  48981