Theorem simp32 1227

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simp132  1326  simp232  1335  simp332  1344  eqfunresadj  7356  smogt  8350  axdc3lem4  10433  bitsfzo  16489  frlmphl  21896  mdetunilem4  22737  mdetuni0  22743  mdetmul  22745  decpmatmullem  22893  logfacbnd3  27349  logexprlim  27351  log2sumbnd  27670  nosupfv  27832  nosupres  27833  noinffv  27847  noinfres  27848  ax5seg  29225  numclwwlk1lem2foa  30642  iocinioc2  33061  totprob  34758  cgrtr  36379  cgrtr3  36381  ofscom  36394  cgrextend  36395  segconeq  36397  ifscgr  36431  colinearxfr  36462  brofs2  36464  brifs2  36465  fscgr  36467  btwnconn1lem2  36475  btwnconn1lem9  36482  btwnconn1lem10  36483  btwnconn1lem11  36484  btwnconn1lem12  36485  brsegle2  36496  seglecgr12im  36497  seglecgr12  36498  segletr  36501  outsideofeq  36517  ivthALT  36731  lshpkrlem5  39773  lshpkrlem6  39774  atbtwnexOLDN  40106  atbtwnex  40107  4noncolr3  40112  3dimlem3a  40119  3dim1  40126  3dim2  40127  1cvrat  40135  2atjlej  40138  hlatexch4  40140  ps-2b  40141  2atm  40186  ps-2c  40187  2atmat  40220  4atlem10  40265  4atlem11b  40267  4atlem11  40268  4at  40272  4at2  40273  2lplnja  40278  2lplnj  40279  dalemswapyz  40315  dalem-ddly  40345  cdlemb  40453  paddasslem5  40483  pmodlem1  40505  dalawlem1  40530  dalawlem3  40532  dalawlem4  40533  dalawlem5  40534  dalawlem6  40535  dalawlem7  40536  dalawlem8  40537  dalawlem9  40538  dalawlem11  40540  dalawlem12  40541  dalawlem15  40544  osumcllem5N  40619  osumcllem6N  40620  lhpexle3lem  40670  lhpmcvr4N  40685  lhpmcvr6N  40687  4atexlemex6  40733  4atex2  40736  4atex2-0bOLDN  40738  4atex2-0cOLDN  40739  ltrn11at  40806  trlval3  40846  cdlemd3  40859  cdleme7aa  40901  cdleme7b  40903  cdleme7c  40904  cdleme7d  40905  cdleme7e  40906  cdleme7ga  40907  cdleme7  40908  cdleme16aN  40918  cdleme11dN  40921  cdleme11e  40922  cdleme11l  40928  cdleme11  40929  cdleme12  40930  cdleme14  40932  cdleme15a  40933  cdleme15c  40935  cdleme16c  40939  cdleme16d  40940  cdleme16e  40941  cdleme16f  40942  cdleme17c  40947  cdleme18c  40952  cdlemeda  40957  cdlemednpq  40958  cdleme19a  40962  cdleme19c  40964  cdleme20aN  40968  cdleme20bN  40969  cdleme20l1  40979  cdleme20l2  40980  cdleme22aa  40998  cdleme22a  40999  cdleme22g  41007  cdleme23b  41009  cdleme23c  41010  cdleme26fALTN  41021  cdleme26f  41022  cdleme26f2ALTN  41023  cdleme26f2  41024  cdleme28b  41030  cdleme32b  41101  cdleme32c  41102  cdleme32e  41104  cdleme35h  41115  cdleme35sn2aw  41117  cdleme38m  41122  cdleme40n  41127  cdleme41sn3aw  41133  cdleme41sn4aw  41134  cdlemeg46gfre  41191  cdlemf1  41220  cdlemg1cex  41247  cdlemg2ce  41251  cdlemg4d  41272  cdlemg4  41276  cdlemg7fvN  41283  cdlemg8b  41287  cdlemg8c  41288  cdlemg9a  41291  cdlemg11aq  41297  cdlemg10a  41299  cdlemg12a  41302  cdlemg12b  41303  cdlemg12d  41305  cdlemg12g  41308  cdlemg12  41309  cdlemg13a  41310  cdlemg13  41311  cdlemg14f  41312  cdlemg14g  41313  cdlemg17b  41321  cdlemg17dN  41322  cdlemg17e  41324  cdlemg17pq  41331  cdlemg17iqN  41333  cdlemg18c  41339  cdlemg18d  41340  cdlemg19a  41342  cdlemg19  41343  cdlemg21  41345  cdlemg27a  41351  cdlemg28a  41352  cdlemg31b0N  41353  cdlemg27b  41355  cdlemg31c  41358  cdlemg33b0  41360  cdlemg28  41363  cdlemg33a  41365  cdlemg33  41370  cdlemg35  41372  cdlemg36  41373  cdlemg44a  41390  cdlemg46  41394  cdlemh2  41475  cdlemh  41476  cdlemj1  41480  cdlemk5  41495  cdlemk6  41496  cdlemki  41500  cdlemksv2  41506  cdlemk7  41507  cdlemk11  41508  cdlemkole  41512  cdlemk14  41513  cdlemk16  41516  cdlemk1u  41518  cdlemk18  41527  cdlemk19  41528  cdlemk7u  41529  cdlemk11u  41530  cdlemk33N  41568  cdlemkid2  41583  cdlemkfid3N  41584  cdlemk11ta  41588  cdlemk11tc  41604  cdlemk45  41606  cdlemk46  41607  cdlemk47  41608  cdlemk52  41613  cdlemk53a  41614  cdlemk54  41617  cdlemk55a  41618  cdleml1N  41635  cdleml3N  41637  cdlemn7  41862  cdlemn8  41863  cdlemn10  41865  dihordlem7  41873  dihordlem7b  41874  dihord1  41877  dihord10  41882  dihord11c  41883  dihord2  41886  hlhilphllem  42618  fmuldfeq  46184  seposep  49582  iscnrm3rlem8  49603  iscnrm3llem2  49606