Theorem simp32 1229

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp132  1328  simp232  1337  simp332  1346  eqfunresadj  7371  smogt  8379  axdc3lem4  10535  bitsfzo  16611  frlmphl  22093  mdetunilem4  22936  mdetuni0  22942  mdetmul  22944  decpmatmullem  23095  logfacbnd3  27556  logexprlim  27558  log2sumbnd  27877  nosupfv  28069  nosupres  28070  noinffv  28084  noinfres  28085  ax5seg  29522  numclwwlk1lem2foa  30961  iocinioc2  33418  totprob  35106  cgrtr  36850  cgrtr3  36852  ofscom  36865  cgrextend  36866  segconeq  36868  ifscgr  36902  colinearxfr  36933  brofs2  36935  brifs2  36936  fscgr  36938  btwnconn1lem2  36946  btwnconn1lem9  36953  btwnconn1lem10  36954  btwnconn1lem11  36955  btwnconn1lem12  36956  brsegle2  36967  seglecgr12im  36968  seglecgr12  36969  segletr  36972  outsideofeq  36988  ivthALT  37216  lshpkrlem5  40265  lshpkrlem6  40266  atbtwnexOLDN  40598  atbtwnex  40599  4noncolr3  40604  3dimlem3a  40611  3dim1  40618  3dim2  40619  1cvrat  40627  2atjlej  40630  hlatexch4  40632  ps-2b  40633  2atm  40678  ps-2c  40679  2atmat  40712  4atlem10  40757  4atlem11b  40759  4atlem11  40760  4at  40764  4at2  40765  2lplnja  40770  2lplnj  40771  dalemswapyz  40807  dalem-ddly  40837  cdlemb  40945  paddasslem5  40975  pmodlem1  40997  dalawlem1  41022  dalawlem3  41024  dalawlem4  41025  dalawlem5  41026  dalawlem6  41027  dalawlem7  41028  dalawlem8  41029  dalawlem9  41030  dalawlem11  41032  dalawlem12  41033  dalawlem15  41036  osumcllem5N  41111  osumcllem6N  41112  lhpexle3lem  41162  lhpmcvr4N  41177  lhpmcvr6N  41179  4atexlemex6  41225  4atex2  41228  4atex2-0bOLDN  41230  4atex2-0cOLDN  41231  ltrn11at  41298  trlval3  41338  cdlemd3  41351  cdleme7aa  41393  cdleme7b  41395  cdleme7c  41396  cdleme7d  41397  cdleme7e  41398  cdleme7ga  41399  cdleme7  41400  cdleme16aN  41410  cdleme11dN  41413  cdleme11e  41414  cdleme11l  41420  cdleme11  41421  cdleme12  41422  cdleme14  41424  cdleme15a  41425  cdleme15c  41427  cdleme16c  41431  cdleme16d  41432  cdleme16e  41433  cdleme16f  41434  cdleme17c  41439  cdleme18c  41444  cdlemeda  41449  cdlemednpq  41450  cdleme19a  41454  cdleme19c  41456  cdleme20aN  41460  cdleme20bN  41461  cdleme20l1  41471  cdleme20l2  41472  cdleme22aa  41490  cdleme22a  41491  cdleme22g  41499  cdleme23b  41501  cdleme23c  41502  cdleme26fALTN  41513  cdleme26f  41514  cdleme26f2ALTN  41515  cdleme26f2  41516  cdleme28b  41522  cdleme32b  41593  cdleme32c  41594  cdleme32e  41596  cdleme35h  41607  cdleme35sn2aw  41609  cdleme38m  41614  cdleme40n  41619  cdleme41sn3aw  41625  cdleme41sn4aw  41626  cdlemeg46gfre  41683  cdlemf1  41712  cdlemg1cex  41739  cdlemg2ce  41743  cdlemg4d  41764  cdlemg4  41768  cdlemg7fvN  41775  cdlemg8b  41779  cdlemg8c  41780  cdlemg9a  41783  cdlemg11aq  41789  cdlemg10a  41791  cdlemg12a  41794  cdlemg12b  41795  cdlemg12d  41797  cdlemg12g  41800  cdlemg12  41801  cdlemg13a  41802  cdlemg13  41803  cdlemg14f  41804  cdlemg14g  41805  cdlemg17b  41813  cdlemg17dN  41814  cdlemg17e  41816  cdlemg17pq  41823  cdlemg17iqN  41825  cdlemg18c  41831  cdlemg18d  41832  cdlemg19a  41834  cdlemg19  41835  cdlemg21  41837  cdlemg27a  41843  cdlemg28a  41844  cdlemg31b0N  41845  cdlemg27b  41847  cdlemg31c  41850  cdlemg33b0  41852  cdlemg28  41855  cdlemg33a  41857  cdlemg33  41862  cdlemg35  41864  cdlemg36  41865  cdlemg44a  41882  cdlemg46  41886  cdlemh2  41967  cdlemh  41968  cdlemj1  41972  cdlemk5  41987  cdlemk6  41988  cdlemki  41992  cdlemksv2  41998  cdlemk7  41999  cdlemk11  42000  cdlemkole  42004  cdlemk14  42005  cdlemk16  42008  cdlemk1u  42010  cdlemk18  42019  cdlemk19  42020  cdlemk7u  42021  cdlemk11u  42022  cdlemk33N  42060  cdlemkid2  42075  cdlemkfid3N  42076  cdlemk11ta  42080  cdlemk11tc  42096  cdlemk45  42098  cdlemk46  42099  cdlemk47  42100  cdlemk52  42105  cdlemk53a  42106  cdlemk54  42109  cdlemk55a  42110  cdleml1N  42127  cdleml3N  42129  cdlemn7  42354  cdlemn8  42355  cdlemn10  42357  dihordlem7  42365  dihordlem7b  42366  dihord1  42369  dihord10  42374  dihord11c  42375  dihord2  42378  hlhilphllem  43110  fmuldfeq  46689  seposep  50134  iscnrm3rlem8  50155  iscnrm3llem2  50158