Theorem simp32 1209

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 1136	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜃)
2	1	3ad2ant3 1134	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  1308  simp232  1317  simp332  1326  eqfunresadj  7379  smogt  8405  axdc3lem4  10490  bitsfzo  16468  frlmphl  21818  mdetunilem4  22636  mdetuni0  22642  mdetmul  22644  decpmatmullem  22792  logfacbnd3  27281  logexprlim  27283  log2sumbnd  27602  nosupfv  27765  nosupres  27766  noinffv  27780  noinfres  27781  ax5seg  28967  numclwwlk1lem2foa  30382  iocinioc2  32787  totprob  34408  cgrtr  35973  cgrtr3  35975  ofscom  35988  cgrextend  35989  segconeq  35991  ifscgr  36025  colinearxfr  36056  brofs2  36058  brifs2  36059  fscgr  36061  btwnconn1lem2  36069  btwnconn1lem9  36076  btwnconn1lem10  36077  btwnconn1lem11  36078  btwnconn1lem12  36079  brsegle2  36090  seglecgr12im  36091  seglecgr12  36092  segletr  36095  outsideofeq  36111  ivthALT  36317  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  41945  fmuldfeq  45538  seposep  48721  iscnrm3rlem8  48743  iscnrm3llem2  48746