Theorem simp32 1211

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

Assertion

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

Proof of Theorem simp32

Step	Hyp	Ref	Expression
1		simp2 1138	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜃)
2	1	3ad2ant3 1136	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  simp132  1310  simp232  1319  simp332  1328  eqfunresadj  7357  smogt  8367  axdc3lem4  10448  bitsfzo  16376  frlmphl  21336  mdetunilem4  22117  mdetuni0  22123  mdetmul  22125  decpmatmullem  22273  logfacbnd3  26726  logexprlim  26728  log2sumbnd  27047  nosupfv  27209  nosupres  27210  noinffv  27224  noinfres  27225  ax5seg  28227  numclwwlk1lem2foa  29638  iocinioc2  32021  totprob  33457  cgrtr  34995  cgrtr3  34997  ofscom  35010  cgrextend  35011  segconeq  35013  ifscgr  35047  colinearxfr  35078  brofs2  35080  brifs2  35081  fscgr  35083  btwnconn1lem2  35091  btwnconn1lem9  35098  btwnconn1lem10  35099  btwnconn1lem11  35100  btwnconn1lem12  35101  brsegle2  35112  seglecgr12im  35113  seglecgr12  35114  segletr  35117  outsideofeq  35133  ivthALT  35268  lshpkrlem5  38032  lshpkrlem6  38033  atbtwnexOLDN  38366  atbtwnex  38367  4noncolr3  38372  3dimlem3a  38379  3dim1  38386  3dim2  38387  1cvrat  38395  2atjlej  38398  hlatexch4  38400  ps-2b  38401  2atm  38446  ps-2c  38447  2atmat  38480  4atlem10  38525  4atlem11b  38527  4atlem11  38528  4at  38532  4at2  38533  2lplnja  38538  2lplnj  38539  dalemswapyz  38575  dalem-ddly  38605  cdlemb  38713  paddasslem5  38743  pmodlem1  38765  dalawlem1  38790  dalawlem3  38792  dalawlem4  38793  dalawlem5  38794  dalawlem6  38795  dalawlem7  38796  dalawlem8  38797  dalawlem9  38798  dalawlem11  38800  dalawlem12  38801  dalawlem15  38804  osumcllem5N  38879  osumcllem6N  38880  lhpexle3lem  38930  lhpmcvr4N  38945  lhpmcvr6N  38947  4atexlemex6  38993  4atex2  38996  4atex2-0bOLDN  38998  4atex2-0cOLDN  38999  ltrn11at  39066  trlval3  39106  cdlemd3  39119  cdleme7aa  39161  cdleme7b  39163  cdleme7c  39164  cdleme7d  39165  cdleme7e  39166  cdleme7ga  39167  cdleme7  39168  cdleme16aN  39178  cdleme11dN  39181  cdleme11e  39182  cdleme11l  39188  cdleme11  39189  cdleme12  39190  cdleme14  39192  cdleme15a  39193  cdleme15c  39195  cdleme16c  39199  cdleme16d  39200  cdleme16e  39201  cdleme16f  39202  cdleme17c  39207  cdleme18c  39212  cdlemeda  39217  cdlemednpq  39218  cdleme19a  39222  cdleme19c  39224  cdleme20aN  39228  cdleme20bN  39229  cdleme20l1  39239  cdleme20l2  39240  cdleme22aa  39258  cdleme22a  39259  cdleme22g  39267  cdleme23b  39269  cdleme23c  39270  cdleme26fALTN  39281  cdleme26f  39282  cdleme26f2ALTN  39283  cdleme26f2  39284  cdleme28b  39290  cdleme32b  39361  cdleme32c  39362  cdleme32e  39364  cdleme35h  39375  cdleme35sn2aw  39377  cdleme38m  39382  cdleme40n  39387  cdleme41sn3aw  39393  cdleme41sn4aw  39394  cdlemeg46gfre  39451  cdlemf1  39480  cdlemg1cex  39507  cdlemg2ce  39511  cdlemg4d  39532  cdlemg4  39536  cdlemg7fvN  39543  cdlemg8b  39547  cdlemg8c  39548  cdlemg9a  39551  cdlemg11aq  39557  cdlemg10a  39559  cdlemg12a  39562  cdlemg12b  39563  cdlemg12d  39565  cdlemg12g  39568  cdlemg12  39569  cdlemg13a  39570  cdlemg13  39571  cdlemg14f  39572  cdlemg14g  39573  cdlemg17b  39581  cdlemg17dN  39582  cdlemg17e  39584  cdlemg17pq  39591  cdlemg17iqN  39593  cdlemg18c  39599  cdlemg18d  39600  cdlemg19a  39602  cdlemg19  39603  cdlemg21  39605  cdlemg27a  39611  cdlemg28a  39612  cdlemg31b0N  39613  cdlemg27b  39615  cdlemg31c  39618  cdlemg33b0  39620  cdlemg28  39623  cdlemg33a  39625  cdlemg33  39630  cdlemg35  39632  cdlemg36  39633  cdlemg44a  39650  cdlemg46  39654  cdlemh2  39735  cdlemh  39736  cdlemj1  39740  cdlemk5  39755  cdlemk6  39756  cdlemki  39760  cdlemksv2  39766  cdlemk7  39767  cdlemk11  39768  cdlemkole  39772  cdlemk14  39773  cdlemk16  39776  cdlemk1u  39778  cdlemk18  39787  cdlemk19  39788  cdlemk7u  39789  cdlemk11u  39790  cdlemk33N  39828  cdlemkid2  39843  cdlemkfid3N  39844  cdlemk11ta  39848  cdlemk11tc  39864  cdlemk45  39866  cdlemk46  39867  cdlemk47  39868  cdlemk52  39873  cdlemk53a  39874  cdlemk54  39877  cdlemk55a  39878  cdleml1N  39895  cdleml3N  39897  cdlemn7  40122  cdlemn8  40123  cdlemn10  40125  dihordlem7  40133  dihordlem7b  40134  dihord1  40137  dihord10  40142  dihord11c  40143  dihord2  40146  hlhilphllem  40882  fmuldfeq  44347  seposep  47606  iscnrm3rlem8  47628  iscnrm3llem2  47631