Theorem simp32 1207

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  simp132  1306  simp232  1315  simp332  1324  eqfunresadj  7372  smogt  8397  axdc3lem4  10496  bitsfzo  16435  frlmphl  21779  mdetunilem4  22608  mdetuni0  22614  mdetmul  22616  decpmatmullem  22764  logfacbnd3  27252  logexprlim  27254  log2sumbnd  27573  nosupfv  27736  nosupres  27737  noinffv  27751  noinfres  27752  ax5seg  28872  numclwwlk1lem2foa  30287  iocinioc2  32681  totprob  34261  cgrtr  35816  cgrtr3  35818  ofscom  35831  cgrextend  35832  segconeq  35834  ifscgr  35868  colinearxfr  35899  brofs2  35901  brifs2  35902  fscgr  35904  btwnconn1lem2  35912  btwnconn1lem9  35919  btwnconn1lem10  35920  btwnconn1lem11  35921  btwnconn1lem12  35922  brsegle2  35933  seglecgr12im  35934  seglecgr12  35935  segletr  35938  outsideofeq  35954  ivthALT  36047  lshpkrlem5  38812  lshpkrlem6  38813  atbtwnexOLDN  39146  atbtwnex  39147  4noncolr3  39152  3dimlem3a  39159  3dim1  39166  3dim2  39167  1cvrat  39175  2atjlej  39178  hlatexch4  39180  ps-2b  39181  2atm  39226  ps-2c  39227  2atmat  39260  4atlem10  39305  4atlem11b  39307  4atlem11  39308  4at  39312  4at2  39313  2lplnja  39318  2lplnj  39319  dalemswapyz  39355  dalem-ddly  39385  cdlemb  39493  paddasslem5  39523  pmodlem1  39545  dalawlem1  39570  dalawlem3  39572  dalawlem4  39573  dalawlem5  39574  dalawlem6  39575  dalawlem7  39576  dalawlem8  39577  dalawlem9  39578  dalawlem11  39580  dalawlem12  39581  dalawlem15  39584  osumcllem5N  39659  osumcllem6N  39660  lhpexle3lem  39710  lhpmcvr4N  39725  lhpmcvr6N  39727  4atexlemex6  39773  4atex2  39776  4atex2-0bOLDN  39778  4atex2-0cOLDN  39779  ltrn11at  39846  trlval3  39886  cdlemd3  39899  cdleme7aa  39941  cdleme7b  39943  cdleme7c  39944  cdleme7d  39945  cdleme7e  39946  cdleme7ga  39947  cdleme7  39948  cdleme16aN  39958  cdleme11dN  39961  cdleme11e  39962  cdleme11l  39968  cdleme11  39969  cdleme12  39970  cdleme14  39972  cdleme15a  39973  cdleme15c  39975  cdleme16c  39979  cdleme16d  39980  cdleme16e  39981  cdleme16f  39982  cdleme17c  39987  cdleme18c  39992  cdlemeda  39997  cdlemednpq  39998  cdleme19a  40002  cdleme19c  40004  cdleme20aN  40008  cdleme20bN  40009  cdleme20l1  40019  cdleme20l2  40020  cdleme22aa  40038  cdleme22a  40039  cdleme22g  40047  cdleme23b  40049  cdleme23c  40050  cdleme26fALTN  40061  cdleme26f  40062  cdleme26f2ALTN  40063  cdleme26f2  40064  cdleme28b  40070  cdleme32b  40141  cdleme32c  40142  cdleme32e  40144  cdleme35h  40155  cdleme35sn2aw  40157  cdleme38m  40162  cdleme40n  40167  cdleme41sn3aw  40173  cdleme41sn4aw  40174  cdlemeg46gfre  40231  cdlemf1  40260  cdlemg1cex  40287  cdlemg2ce  40291  cdlemg4d  40312  cdlemg4  40316  cdlemg7fvN  40323  cdlemg8b  40327  cdlemg8c  40328  cdlemg9a  40331  cdlemg11aq  40337  cdlemg10a  40339  cdlemg12a  40342  cdlemg12b  40343  cdlemg12d  40345  cdlemg12g  40348  cdlemg12  40349  cdlemg13a  40350  cdlemg13  40351  cdlemg14f  40352  cdlemg14g  40353  cdlemg17b  40361  cdlemg17dN  40362  cdlemg17e  40364  cdlemg17pq  40371  cdlemg17iqN  40373  cdlemg18c  40379  cdlemg18d  40380  cdlemg19a  40382  cdlemg19  40383  cdlemg21  40385  cdlemg27a  40391  cdlemg28a  40392  cdlemg31b0N  40393  cdlemg27b  40395  cdlemg31c  40398  cdlemg33b0  40400  cdlemg28  40403  cdlemg33a  40405  cdlemg33  40410  cdlemg35  40412  cdlemg36  40413  cdlemg44a  40430  cdlemg46  40434  cdlemh2  40515  cdlemh  40516  cdlemj1  40520  cdlemk5  40535  cdlemk6  40536  cdlemki  40540  cdlemksv2  40546  cdlemk7  40547  cdlemk11  40548  cdlemkole  40552  cdlemk14  40553  cdlemk16  40556  cdlemk1u  40558  cdlemk18  40567  cdlemk19  40568  cdlemk7u  40569  cdlemk11u  40570  cdlemk33N  40608  cdlemkid2  40623  cdlemkfid3N  40624  cdlemk11ta  40628  cdlemk11tc  40644  cdlemk45  40646  cdlemk46  40647  cdlemk47  40648  cdlemk52  40653  cdlemk53a  40654  cdlemk54  40657  cdlemk55a  40658  cdleml1N  40675  cdleml3N  40677  cdlemn7  40902  cdlemn8  40903  cdlemn10  40905  dihordlem7  40913  dihordlem7b  40914  dihord1  40917  dihord10  40922  dihord11c  40923  dihord2  40926  hlhilphllem  41662  fmuldfeq  45204  seposep  48259  iscnrm3rlem8  48281  iscnrm3llem2  48284