Theorem simp32 1206

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp132  1305  simp232  1314  simp332  1323  smogt  8004  axdc3lem4  9875  bitsfzo  15784  frlmphl  20925  mdetunilem4  21224  mdetuni0  21230  mdetmul  21232  decpmatmullem  21379  logfacbnd3  25799  logexprlim  25801  log2sumbnd  26120  ax5seg  26724  numclwwlk1lem2foa  28133  iocinioc2  30502  totprob  31685  eqfunresadj  33004  nosupfv  33206  nosupres  33207  cgrtr  33453  cgrtr3  33455  ofscom  33468  cgrextend  33469  segconeq  33471  ifscgr  33505  colinearxfr  33536  brofs2  33538  brifs2  33539  fscgr  33541  btwnconn1lem2  33549  btwnconn1lem9  33556  btwnconn1lem10  33557  btwnconn1lem11  33558  btwnconn1lem12  33559  brsegle2  33570  seglecgr12im  33571  seglecgr12  33572  segletr  33575  outsideofeq  33591  ivthALT  33683  lshpkrlem5  36265  lshpkrlem6  36266  atbtwnexOLDN  36598  atbtwnex  36599  4noncolr3  36604  3dimlem3a  36611  3dim1  36618  3dim2  36619  1cvrat  36627  2atjlej  36630  hlatexch4  36632  ps-2b  36633  2atm  36678  ps-2c  36679  2atmat  36712  4atlem10  36757  4atlem11b  36759  4atlem11  36760  4at  36764  4at2  36765  2lplnja  36770  2lplnj  36771  dalemswapyz  36807  dalem-ddly  36837  cdlemb  36945  paddasslem5  36975  pmodlem1  36997  dalawlem1  37022  dalawlem3  37024  dalawlem4  37025  dalawlem5  37026  dalawlem6  37027  dalawlem7  37028  dalawlem8  37029  dalawlem9  37030  dalawlem11  37032  dalawlem12  37033  dalawlem15  37036  osumcllem5N  37111  osumcllem6N  37112  lhpexle3lem  37162  lhpmcvr4N  37177  lhpmcvr6N  37179  4atexlemex6  37225  4atex2  37228  4atex2-0bOLDN  37230  4atex2-0cOLDN  37231  ltrn11at  37298  trlval3  37338  cdlemd3  37351  cdleme7aa  37393  cdleme7b  37395  cdleme7c  37396  cdleme7d  37397  cdleme7e  37398  cdleme7ga  37399  cdleme7  37400  cdleme16aN  37410  cdleme11dN  37413  cdleme11e  37414  cdleme11l  37420  cdleme11  37421  cdleme12  37422  cdleme14  37424  cdleme15a  37425  cdleme15c  37427  cdleme16c  37431  cdleme16d  37432  cdleme16e  37433  cdleme16f  37434  cdleme17c  37439  cdleme18c  37444  cdlemeda  37449  cdlemednpq  37450  cdleme19a  37454  cdleme19c  37456  cdleme20aN  37460  cdleme20bN  37461  cdleme20l1  37471  cdleme20l2  37472  cdleme22aa  37490  cdleme22a  37491  cdleme22g  37499  cdleme23b  37501  cdleme23c  37502  cdleme26fALTN  37513  cdleme26f  37514  cdleme26f2ALTN  37515  cdleme26f2  37516  cdleme28b  37522  cdleme32b  37593  cdleme32c  37594  cdleme32e  37596  cdleme35h  37607  cdleme35sn2aw  37609  cdleme38m  37614  cdleme40n  37619  cdleme41sn3aw  37625  cdleme41sn4aw  37626  cdlemeg46gfre  37683  cdlemf1  37712  cdlemg1cex  37739  cdlemg2ce  37743  cdlemg4d  37764  cdlemg4  37768  cdlemg7fvN  37775  cdlemg8b  37779  cdlemg8c  37780  cdlemg9a  37783  cdlemg11aq  37789  cdlemg10a  37791  cdlemg12a  37794  cdlemg12b  37795  cdlemg12d  37797  cdlemg12g  37800  cdlemg12  37801  cdlemg13a  37802  cdlemg13  37803  cdlemg14f  37804  cdlemg14g  37805  cdlemg17b  37813  cdlemg17dN  37814  cdlemg17e  37816  cdlemg17pq  37823  cdlemg17iqN  37825  cdlemg18c  37831  cdlemg18d  37832  cdlemg19a  37834  cdlemg19  37835  cdlemg21  37837  cdlemg27a  37843  cdlemg28a  37844  cdlemg31b0N  37845  cdlemg27b  37847  cdlemg31c  37850  cdlemg33b0  37852  cdlemg28  37855  cdlemg33a  37857  cdlemg33  37862  cdlemg35  37864  cdlemg36  37865  cdlemg44a  37882  cdlemg46  37886  cdlemh2  37967  cdlemh  37968  cdlemj1  37972  cdlemk5  37987  cdlemk6  37988  cdlemki  37992  cdlemksv2  37998  cdlemk7  37999  cdlemk11  38000  cdlemkole  38004  cdlemk14  38005  cdlemk16  38008  cdlemk1u  38010  cdlemk18  38019  cdlemk19  38020  cdlemk7u  38021  cdlemk11u  38022  cdlemk33N  38060  cdlemkid2  38075  cdlemkfid3N  38076  cdlemk11ta  38080  cdlemk11tc  38096  cdlemk45  38098  cdlemk46  38099  cdlemk47  38100  cdlemk52  38105  cdlemk53a  38106  cdlemk54  38109  cdlemk55a  38110  cdleml1N  38127  cdleml3N  38129  cdlemn7  38354  cdlemn8  38355  cdlemn10  38357  dihordlem7  38365  dihordlem7b  38366  dihord1  38369  dihord10  38374  dihord11c  38375  dihord2  38378  hlhilphllem  39110  fmuldfeq  41884