Theorem simp32 1224

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

Syntax hints:   → wi 4   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  simpl32OLD  1301  simpr32OLD  1319  simp132  1365  simp232  1374  simp332  1383  smogt  7749  axdc3lem4  9612  bitsfzo  15573  frlmphl  20535  mdetunilem4  20837  mdetuni0  20843  mdetmul  20845  decpmatmullem  20994  logfacbnd3  25411  logexprlim  25413  log2sumbnd  25702  ax5seg  26304  numclwwlk1lem2foa  27786  numclwwlk1lem2foaOLD  27787  iocinioc2  30119  totprob  31096  eqfunresadj  32260  nosupfv  32449  nosupres  32450  cgrtr  32696  cgrtr3  32698  ofscom  32711  cgrextend  32712  segconeq  32714  ifscgr  32748  colinearxfr  32779  brofs2  32781  brifs2  32782  fscgr  32784  btwnconn1lem2  32792  btwnconn1lem9  32799  btwnconn1lem10  32800  btwnconn1lem11  32801  btwnconn1lem12  32802  brsegle2  32813  seglecgr12im  32814  seglecgr12  32815  segletr  32818  outsideofeq  32834  ivthALT  32926  lshpkrlem5  35277  lshpkrlem6  35278  atbtwnexOLDN  35610  atbtwnex  35611  4noncolr3  35616  3dimlem3a  35623  3dim1  35630  3dim2  35631  1cvrat  35639  2atjlej  35642  hlatexch4  35644  ps-2b  35645  2atm  35690  ps-2c  35691  2atmat  35724  4atlem10  35769  4atlem11b  35771  4atlem11  35772  4at  35776  4at2  35777  2lplnja  35782  2lplnj  35783  dalemswapyz  35819  dalem-ddly  35849  cdlemb  35957  paddasslem5  35987  pmodlem1  36009  dalawlem1  36034  dalawlem3  36036  dalawlem4  36037  dalawlem5  36038  dalawlem6  36039  dalawlem7  36040  dalawlem8  36041  dalawlem9  36042  dalawlem11  36044  dalawlem12  36045  dalawlem15  36048  osumcllem5N  36123  osumcllem6N  36124  lhpexle3lem  36174  lhpmcvr4N  36189  lhpmcvr6N  36191  4atexlemex6  36237  4atex2  36240  4atex2-0bOLDN  36242  4atex2-0cOLDN  36243  ltrn11at  36310  trlval3  36350  cdlemd3  36363  cdleme7aa  36405  cdleme7b  36407  cdleme7c  36408  cdleme7d  36409  cdleme7e  36410  cdleme7ga  36411  cdleme7  36412  cdleme16aN  36422  cdleme11dN  36425  cdleme11e  36426  cdleme11l  36432  cdleme11  36433  cdleme12  36434  cdleme14  36436  cdleme15a  36437  cdleme15c  36439  cdleme16c  36443  cdleme16d  36444  cdleme16e  36445  cdleme16f  36446  cdleme17c  36451  cdleme18c  36456  cdlemeda  36461  cdlemednpq  36462  cdleme19a  36466  cdleme19c  36468  cdleme20aN  36472  cdleme20bN  36473  cdleme20l1  36483  cdleme20l2  36484  cdleme22aa  36502  cdleme22a  36503  cdleme22g  36511  cdleme23b  36513  cdleme23c  36514  cdleme26fALTN  36525  cdleme26f  36526  cdleme26f2ALTN  36527  cdleme26f2  36528  cdleme28b  36534  cdleme32b  36605  cdleme32c  36606  cdleme32e  36608  cdleme35h  36619  cdleme35sn2aw  36621  cdleme38m  36626  cdleme40n  36631  cdleme41sn3aw  36637  cdleme41sn4aw  36638  cdlemeg46gfre  36695  cdlemf1  36724  cdlemg1cex  36751  cdlemg2ce  36755  cdlemg4d  36776  cdlemg4  36780  cdlemg7fvN  36787  cdlemg8b  36791  cdlemg8c  36792  cdlemg9a  36795  cdlemg11aq  36801  cdlemg10a  36803  cdlemg12a  36806  cdlemg12b  36807  cdlemg12d  36809  cdlemg12g  36812  cdlemg12  36813  cdlemg13a  36814  cdlemg13  36815  cdlemg14f  36816  cdlemg14g  36817  cdlemg17b  36825  cdlemg17dN  36826  cdlemg17e  36828  cdlemg17pq  36835  cdlemg17iqN  36837  cdlemg18c  36843  cdlemg18d  36844  cdlemg19a  36846  cdlemg19  36847  cdlemg21  36849  cdlemg27a  36855  cdlemg28a  36856  cdlemg31b0N  36857  cdlemg27b  36859  cdlemg31c  36862  cdlemg33b0  36864  cdlemg28  36867  cdlemg33a  36869  cdlemg33  36874  cdlemg35  36876  cdlemg36  36877  cdlemg44a  36894  cdlemg46  36898  cdlemh2  36979  cdlemh  36980  cdlemj1  36984  cdlemk5  36999  cdlemk6  37000  cdlemki  37004  cdlemksv2  37010  cdlemk7  37011  cdlemk11  37012  cdlemkole  37016  cdlemk14  37017  cdlemk16  37020  cdlemk1u  37022  cdlemk18  37031  cdlemk19  37032  cdlemk7u  37033  cdlemk11u  37034  cdlemk33N  37072  cdlemkid2  37087  cdlemkfid3N  37088  cdlemk11ta  37092  cdlemk11tc  37108  cdlemk45  37110  cdlemk46  37111  cdlemk47  37112  cdlemk52  37117  cdlemk53a  37118  cdlemk54  37121  cdlemk55a  37122  cdleml1N  37139  cdleml3N  37141  cdlemn7  37366  cdlemn8  37367  cdlemn10  37369  dihordlem7  37377  dihordlem7b  37378  dihord1  37381  dihord10  37386  dihord11c  37387  dihord2  37390  hlhilphllem  38122  fmuldfeq  40737