Theorem simp32 1212

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp132  1311  simp232  1320  simp332  1329  eqfunresadj  7315  smogt  8307  axdc3lem4  10375  bitsfzo  16404  frlmphl  21761  mdetunilem4  22580  mdetuni0  22586  mdetmul  22588  decpmatmullem  22736  logfacbnd3  27186  logexprlim  27188  log2sumbnd  27507  nosupfv  27670  nosupres  27671  noinffv  27685  noinfres  27686  ax5seg  29007  numclwwlk1lem2foa  30424  iocinioc2  32852  totprob  34571  cgrtr  36174  cgrtr3  36176  ofscom  36189  cgrextend  36190  segconeq  36192  ifscgr  36226  colinearxfr  36257  brofs2  36259  brifs2  36260  fscgr  36262  btwnconn1lem2  36270  btwnconn1lem9  36277  btwnconn1lem10  36278  btwnconn1lem11  36279  btwnconn1lem12  36280  brsegle2  36291  seglecgr12im  36292  seglecgr12  36293  segletr  36296  outsideofeq  36312  ivthALT  36517  lshpkrlem5  39560  lshpkrlem6  39561  atbtwnexOLDN  39893  atbtwnex  39894  4noncolr3  39899  3dimlem3a  39906  3dim1  39913  3dim2  39914  1cvrat  39922  2atjlej  39925  hlatexch4  39927  ps-2b  39928  2atm  39973  ps-2c  39974  2atmat  40007  4atlem10  40052  4atlem11b  40054  4atlem11  40055  4at  40059  4at2  40060  2lplnja  40065  2lplnj  40066  dalemswapyz  40102  dalem-ddly  40132  cdlemb  40240  paddasslem5  40270  pmodlem1  40292  dalawlem1  40317  dalawlem3  40319  dalawlem4  40320  dalawlem5  40321  dalawlem6  40322  dalawlem7  40323  dalawlem8  40324  dalawlem9  40325  dalawlem11  40327  dalawlem12  40328  dalawlem15  40331  osumcllem5N  40406  osumcllem6N  40407  lhpexle3lem  40457  lhpmcvr4N  40472  lhpmcvr6N  40474  4atexlemex6  40520  4atex2  40523  4atex2-0bOLDN  40525  4atex2-0cOLDN  40526  ltrn11at  40593  trlval3  40633  cdlemd3  40646  cdleme7aa  40688  cdleme7b  40690  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme16aN  40705  cdleme11dN  40708  cdleme11e  40709  cdleme11l  40715  cdleme11  40716  cdleme12  40717  cdleme14  40719  cdleme15a  40720  cdleme15c  40722  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme16f  40729  cdleme17c  40734  cdleme18c  40739  cdlemeda  40744  cdlemednpq  40745  cdleme19a  40749  cdleme19c  40751  cdleme20aN  40755  cdleme20bN  40756  cdleme20l1  40766  cdleme20l2  40767  cdleme22aa  40785  cdleme22a  40786  cdleme22g  40794  cdleme23b  40796  cdleme23c  40797  cdleme26fALTN  40808  cdleme26f  40809  cdleme26f2ALTN  40810  cdleme26f2  40811  cdleme28b  40817  cdleme32b  40888  cdleme32c  40889  cdleme32e  40891  cdleme35h  40902  cdleme35sn2aw  40904  cdleme38m  40909  cdleme40n  40914  cdleme41sn3aw  40920  cdleme41sn4aw  40921  cdlemeg46gfre  40978  cdlemf1  41007  cdlemg1cex  41034  cdlemg2ce  41038  cdlemg4d  41059  cdlemg4  41063  cdlemg7fvN  41070  cdlemg8b  41074  cdlemg8c  41075  cdlemg9a  41078  cdlemg11aq  41084  cdlemg10a  41086  cdlemg12a  41089  cdlemg12b  41090  cdlemg12d  41092  cdlemg12g  41095  cdlemg12  41096  cdlemg13a  41097  cdlemg13  41098  cdlemg14f  41099  cdlemg14g  41100  cdlemg17b  41108  cdlemg17dN  41109  cdlemg17e  41111  cdlemg17pq  41118  cdlemg17iqN  41120  cdlemg18c  41126  cdlemg18d  41127  cdlemg19a  41129  cdlemg19  41130  cdlemg21  41132  cdlemg27a  41138  cdlemg28a  41139  cdlemg31b0N  41140  cdlemg27b  41142  cdlemg31c  41145  cdlemg33b0  41147  cdlemg28  41150  cdlemg33a  41152  cdlemg33  41157  cdlemg35  41159  cdlemg36  41160  cdlemg44a  41177  cdlemg46  41181  cdlemh2  41262  cdlemh  41263  cdlemj1  41267  cdlemk5  41282  cdlemk6  41283  cdlemki  41287  cdlemksv2  41293  cdlemk7  41294  cdlemk11  41295  cdlemkole  41299  cdlemk14  41300  cdlemk16  41303  cdlemk1u  41305  cdlemk18  41314  cdlemk19  41315  cdlemk7u  41316  cdlemk11u  41317  cdlemk33N  41355  cdlemkid2  41370  cdlemkfid3N  41371  cdlemk11ta  41375  cdlemk11tc  41391  cdlemk45  41393  cdlemk46  41394  cdlemk47  41395  cdlemk52  41400  cdlemk53a  41401  cdlemk54  41404  cdlemk55a  41405  cdleml1N  41422  cdleml3N  41424  cdlemn7  41649  cdlemn8  41650  cdlemn10  41652  dihordlem7  41660  dihordlem7b  41661  dihord1  41664  dihord10  41669  dihord11c  41670  dihord2  41673  hlhilphllem  42405  fmuldfeq  46013  seposep  49401  iscnrm3rlem8  49422  iscnrm3llem2  49425