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  7366  smogt  8356  axdc3lem4  10448  bitsfzo  16510  frlmphl  21960  mdetunilem4  22801  mdetuni0  22807  mdetmul  22809  decpmatmullem  22957  logfacbnd3  27416  logexprlim  27418  log2sumbnd  27737  nosupfv  27899  nosupres  27900  noinffv  27914  noinfres  27915  ax5seg  29317  numclwwlk1lem2foa  30734  iocinioc2  33153  totprob  34841  cgrtr  36497  cgrtr3  36499  ofscom  36512  cgrextend  36513  segconeq  36515  ifscgr  36549  colinearxfr  36580  brofs2  36582  brifs2  36583  fscgr  36585  btwnconn1lem2  36593  btwnconn1lem9  36600  btwnconn1lem10  36601  btwnconn1lem11  36602  btwnconn1lem12  36603  brsegle2  36614  seglecgr12im  36615  seglecgr12  36616  segletr  36619  outsideofeq  36635  ivthALT  36879  lshpkrlem5  39921  lshpkrlem6  39922  atbtwnexOLDN  40254  atbtwnex  40255  4noncolr3  40260  3dimlem3a  40267  3dim1  40274  3dim2  40275  1cvrat  40283  2atjlej  40286  hlatexch4  40288  ps-2b  40289  2atm  40334  ps-2c  40335  2atmat  40368  4atlem10  40413  4atlem11b  40415  4atlem11  40416  4at  40420  4at2  40421  2lplnja  40426  2lplnj  40427  dalemswapyz  40463  dalem-ddly  40493  cdlemb  40601  paddasslem5  40631  pmodlem1  40653  dalawlem1  40678  dalawlem3  40680  dalawlem4  40681  dalawlem5  40682  dalawlem6  40683  dalawlem7  40684  dalawlem8  40685  dalawlem9  40686  dalawlem11  40688  dalawlem12  40689  dalawlem15  40692  osumcllem5N  40767  osumcllem6N  40768  lhpexle3lem  40818  lhpmcvr4N  40833  lhpmcvr6N  40835  4atexlemex6  40881  4atex2  40884  4atex2-0bOLDN  40886  4atex2-0cOLDN  40887  ltrn11at  40954  trlval3  40994  cdlemd3  41007  cdleme7aa  41049  cdleme7b  41051  cdleme7c  41052  cdleme7d  41053  cdleme7e  41054  cdleme7ga  41055  cdleme7  41056  cdleme16aN  41066  cdleme11dN  41069  cdleme11e  41070  cdleme11l  41076  cdleme11  41077  cdleme12  41078  cdleme14  41080  cdleme15a  41081  cdleme15c  41083  cdleme16c  41087  cdleme16d  41088  cdleme16e  41089  cdleme16f  41090  cdleme17c  41095  cdleme18c  41100  cdlemeda  41105  cdlemednpq  41106  cdleme19a  41110  cdleme19c  41112  cdleme20aN  41116  cdleme20bN  41117  cdleme20l1  41127  cdleme20l2  41128  cdleme22aa  41146  cdleme22a  41147  cdleme22g  41155  cdleme23b  41157  cdleme23c  41158  cdleme26fALTN  41169  cdleme26f  41170  cdleme26f2ALTN  41171  cdleme26f2  41172  cdleme28b  41178  cdleme32b  41249  cdleme32c  41250  cdleme32e  41252  cdleme35h  41263  cdleme35sn2aw  41265  cdleme38m  41270  cdleme40n  41275  cdleme41sn3aw  41281  cdleme41sn4aw  41282  cdlemeg46gfre  41339  cdlemf1  41368  cdlemg1cex  41395  cdlemg2ce  41399  cdlemg4d  41420  cdlemg4  41424  cdlemg7fvN  41431  cdlemg8b  41435  cdlemg8c  41436  cdlemg9a  41439  cdlemg11aq  41445  cdlemg10a  41447  cdlemg12a  41450  cdlemg12b  41451  cdlemg12d  41453  cdlemg12g  41456  cdlemg12  41457  cdlemg13a  41458  cdlemg13  41459  cdlemg14f  41460  cdlemg14g  41461  cdlemg17b  41469  cdlemg17dN  41470  cdlemg17e  41472  cdlemg17pq  41479  cdlemg17iqN  41481  cdlemg18c  41487  cdlemg18d  41488  cdlemg19a  41490  cdlemg19  41491  cdlemg21  41493  cdlemg27a  41499  cdlemg28a  41500  cdlemg31b0N  41501  cdlemg27b  41503  cdlemg31c  41506  cdlemg33b0  41508  cdlemg28  41511  cdlemg33a  41513  cdlemg33  41518  cdlemg35  41520  cdlemg36  41521  cdlemg44a  41538  cdlemg46  41542  cdlemh2  41623  cdlemh  41624  cdlemj1  41628  cdlemk5  41643  cdlemk6  41644  cdlemki  41648  cdlemksv2  41654  cdlemk7  41655  cdlemk11  41656  cdlemkole  41660  cdlemk14  41661  cdlemk16  41664  cdlemk1u  41666  cdlemk18  41675  cdlemk19  41676  cdlemk7u  41677  cdlemk11u  41678  cdlemk33N  41716  cdlemkid2  41731  cdlemkfid3N  41732  cdlemk11ta  41736  cdlemk11tc  41752  cdlemk45  41754  cdlemk46  41755  cdlemk47  41756  cdlemk52  41761  cdlemk53a  41762  cdlemk54  41765  cdlemk55a  41766  cdleml1N  41783  cdleml3N  41785  cdlemn7  42010  cdlemn8  42011  cdlemn10  42013  dihordlem7  42021  dihordlem7b  42022  dihord1  42025  dihord10  42030  dihord11c  42031  dihord2  42034  hlhilphllem  42766  fmuldfeq  46332  seposep  49737  iscnrm3rlem8  49758  iscnrm3llem2  49761