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 1137	. 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:  simp132  1310  simp232  1319  simp332  1328  eqfunresadj  7301  smogt  8297  axdc3lem4  10366  bitsfzo  16364  frlmphl  21706  mdetunilem4  22518  mdetuni0  22524  mdetmul  22526  decpmatmullem  22674  logfacbnd3  27150  logexprlim  27152  log2sumbnd  27471  nosupfv  27634  nosupres  27635  noinffv  27649  noinfres  27650  ax5seg  28901  numclwwlk1lem2foa  30316  iocinioc2  32735  totprob  34397  cgrtr  35968  cgrtr3  35970  ofscom  35983  cgrextend  35984  segconeq  35986  ifscgr  36020  colinearxfr  36051  brofs2  36053  brifs2  36054  fscgr  36056  btwnconn1lem2  36064  btwnconn1lem9  36071  btwnconn1lem10  36072  btwnconn1lem11  36073  btwnconn1lem12  36074  brsegle2  36085  seglecgr12im  36086  seglecgr12  36087  segletr  36090  outsideofeq  36106  ivthALT  36311  lshpkrlem5  39095  lshpkrlem6  39096  atbtwnexOLDN  39429  atbtwnex  39430  4noncolr3  39435  3dimlem3a  39442  3dim1  39449  3dim2  39450  1cvrat  39458  2atjlej  39461  hlatexch4  39463  ps-2b  39464  2atm  39509  ps-2c  39510  2atmat  39543  4atlem10  39588  4atlem11b  39590  4atlem11  39591  4at  39595  4at2  39596  2lplnja  39601  2lplnj  39602  dalemswapyz  39638  dalem-ddly  39668  cdlemb  39776  paddasslem5  39806  pmodlem1  39828  dalawlem1  39853  dalawlem3  39855  dalawlem4  39856  dalawlem5  39857  dalawlem6  39858  dalawlem7  39859  dalawlem8  39860  dalawlem9  39861  dalawlem11  39863  dalawlem12  39864  dalawlem15  39867  osumcllem5N  39942  osumcllem6N  39943  lhpexle3lem  39993  lhpmcvr4N  40008  lhpmcvr6N  40010  4atexlemex6  40056  4atex2  40059  4atex2-0bOLDN  40061  4atex2-0cOLDN  40062  ltrn11at  40129  trlval3  40169  cdlemd3  40182  cdleme7aa  40224  cdleme7b  40226  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme16aN  40241  cdleme11dN  40244  cdleme11e  40245  cdleme11l  40251  cdleme11  40252  cdleme12  40253  cdleme14  40255  cdleme15a  40256  cdleme15c  40258  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme16f  40265  cdleme17c  40270  cdleme18c  40275  cdlemeda  40280  cdlemednpq  40281  cdleme19a  40285  cdleme19c  40287  cdleme20aN  40291  cdleme20bN  40292  cdleme20l1  40302  cdleme20l2  40303  cdleme22aa  40321  cdleme22a  40322  cdleme22g  40330  cdleme23b  40332  cdleme23c  40333  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdleme28b  40353  cdleme32b  40424  cdleme32c  40425  cdleme32e  40427  cdleme35h  40438  cdleme35sn2aw  40440  cdleme38m  40445  cdleme40n  40450  cdleme41sn3aw  40456  cdleme41sn4aw  40457  cdlemeg46gfre  40514  cdlemf1  40543  cdlemg1cex  40570  cdlemg2ce  40574  cdlemg4d  40595  cdlemg4  40599  cdlemg7fvN  40606  cdlemg8b  40610  cdlemg8c  40611  cdlemg9a  40614  cdlemg11aq  40620  cdlemg10a  40622  cdlemg12a  40625  cdlemg12b  40626  cdlemg12d  40628  cdlemg12g  40631  cdlemg12  40632  cdlemg13a  40633  cdlemg13  40634  cdlemg14f  40635  cdlemg14g  40636  cdlemg17b  40644  cdlemg17dN  40645  cdlemg17e  40647  cdlemg17pq  40654  cdlemg17iqN  40656  cdlemg18c  40662  cdlemg18d  40663  cdlemg19a  40665  cdlemg19  40666  cdlemg21  40668  cdlemg27a  40674  cdlemg28a  40675  cdlemg31b0N  40676  cdlemg27b  40678  cdlemg31c  40681  cdlemg33b0  40683  cdlemg28  40686  cdlemg33a  40688  cdlemg33  40693  cdlemg35  40695  cdlemg36  40696  cdlemg44a  40713  cdlemg46  40717  cdlemh2  40798  cdlemh  40799  cdlemj1  40803  cdlemk5  40818  cdlemk6  40819  cdlemki  40823  cdlemksv2  40829  cdlemk7  40830  cdlemk11  40831  cdlemkole  40835  cdlemk14  40836  cdlemk16  40839  cdlemk1u  40841  cdlemk18  40850  cdlemk19  40851  cdlemk7u  40852  cdlemk11u  40853  cdlemk33N  40891  cdlemkid2  40906  cdlemkfid3N  40907  cdlemk11ta  40911  cdlemk11tc  40927  cdlemk45  40929  cdlemk46  40930  cdlemk47  40931  cdlemk52  40936  cdlemk53a  40937  cdlemk54  40940  cdlemk55a  40941  cdleml1N  40958  cdleml3N  40960  cdlemn7  41185  cdlemn8  41186  cdlemn10  41188  dihordlem7  41196  dihordlem7b  41197  dihord1  41200  dihord10  41205  dihord11c  41206  dihord2  41209  hlhilphllem  41941  fmuldfeq  45568  seposep  48914  iscnrm3rlem8  48935  iscnrm3llem2  48938