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  7306  smogt  8298  axdc3lem4  10364  bitsfzo  16363  frlmphl  21738  mdetunilem4  22558  mdetuni0  22564  mdetmul  22566  decpmatmullem  22714  logfacbnd3  27174  logexprlim  27176  log2sumbnd  27495  nosupfv  27658  nosupres  27659  noinffv  27673  noinfres  27674  ax5seg  28995  numclwwlk1lem2foa  30413  iocinioc2  32842  totprob  34577  cgrtr  36180  cgrtr3  36182  ofscom  36195  cgrextend  36196  segconeq  36198  ifscgr  36232  colinearxfr  36263  brofs2  36265  brifs2  36266  fscgr  36268  btwnconn1lem2  36276  btwnconn1lem9  36283  btwnconn1lem10  36284  btwnconn1lem11  36285  btwnconn1lem12  36286  brsegle2  36297  seglecgr12im  36298  seglecgr12  36299  segletr  36302  outsideofeq  36318  ivthALT  36523  lshpkrlem5  39551  lshpkrlem6  39552  atbtwnexOLDN  39884  atbtwnex  39885  4noncolr3  39890  3dimlem3a  39897  3dim1  39904  3dim2  39905  1cvrat  39913  2atjlej  39916  hlatexch4  39918  ps-2b  39919  2atm  39964  ps-2c  39965  2atmat  39998  4atlem10  40043  4atlem11b  40045  4atlem11  40046  4at  40050  4at2  40051  2lplnja  40056  2lplnj  40057  dalemswapyz  40093  dalem-ddly  40123  cdlemb  40231  paddasslem5  40261  pmodlem1  40283  dalawlem1  40308  dalawlem3  40310  dalawlem4  40311  dalawlem5  40312  dalawlem6  40313  dalawlem7  40314  dalawlem8  40315  dalawlem9  40316  dalawlem11  40318  dalawlem12  40319  dalawlem15  40322  osumcllem5N  40397  osumcllem6N  40398  lhpexle3lem  40448  lhpmcvr4N  40463  lhpmcvr6N  40465  4atexlemex6  40511  4atex2  40514  4atex2-0bOLDN  40516  4atex2-0cOLDN  40517  ltrn11at  40584  trlval3  40624  cdlemd3  40637  cdleme7aa  40679  cdleme7b  40681  cdleme7c  40682  cdleme7d  40683  cdleme7e  40684  cdleme7ga  40685  cdleme7  40686  cdleme16aN  40696  cdleme11dN  40699  cdleme11e  40700  cdleme11l  40706  cdleme11  40707  cdleme12  40708  cdleme14  40710  cdleme15a  40711  cdleme15c  40713  cdleme16c  40717  cdleme16d  40718  cdleme16e  40719  cdleme16f  40720  cdleme17c  40725  cdleme18c  40730  cdlemeda  40735  cdlemednpq  40736  cdleme19a  40740  cdleme19c  40742  cdleme20aN  40746  cdleme20bN  40747  cdleme20l1  40757  cdleme20l2  40758  cdleme22aa  40776  cdleme22a  40777  cdleme22g  40785  cdleme23b  40787  cdleme23c  40788  cdleme26fALTN  40799  cdleme26f  40800  cdleme26f2ALTN  40801  cdleme26f2  40802  cdleme28b  40808  cdleme32b  40879  cdleme32c  40880  cdleme32e  40882  cdleme35h  40893  cdleme35sn2aw  40895  cdleme38m  40900  cdleme40n  40905  cdleme41sn3aw  40911  cdleme41sn4aw  40912  cdlemeg46gfre  40969  cdlemf1  40998  cdlemg1cex  41025  cdlemg2ce  41029  cdlemg4d  41050  cdlemg4  41054  cdlemg7fvN  41061  cdlemg8b  41065  cdlemg8c  41066  cdlemg9a  41069  cdlemg11aq  41075  cdlemg10a  41077  cdlemg12a  41080  cdlemg12b  41081  cdlemg12d  41083  cdlemg12g  41086  cdlemg12  41087  cdlemg13a  41088  cdlemg13  41089  cdlemg14f  41090  cdlemg14g  41091  cdlemg17b  41099  cdlemg17dN  41100  cdlemg17e  41102  cdlemg17pq  41109  cdlemg17iqN  41111  cdlemg18c  41117  cdlemg18d  41118  cdlemg19a  41120  cdlemg19  41121  cdlemg21  41123  cdlemg27a  41129  cdlemg28a  41130  cdlemg31b0N  41131  cdlemg27b  41133  cdlemg31c  41136  cdlemg33b0  41138  cdlemg28  41141  cdlemg33a  41143  cdlemg33  41148  cdlemg35  41150  cdlemg36  41151  cdlemg44a  41168  cdlemg46  41172  cdlemh2  41253  cdlemh  41254  cdlemj1  41258  cdlemk5  41273  cdlemk6  41274  cdlemki  41278  cdlemksv2  41284  cdlemk7  41285  cdlemk11  41286  cdlemkole  41290  cdlemk14  41291  cdlemk16  41294  cdlemk1u  41296  cdlemk18  41305  cdlemk19  41306  cdlemk7u  41307  cdlemk11u  41308  cdlemk33N  41346  cdlemkid2  41361  cdlemkfid3N  41362  cdlemk11ta  41366  cdlemk11tc  41382  cdlemk45  41384  cdlemk46  41385  cdlemk47  41386  cdlemk52  41391  cdlemk53a  41392  cdlemk54  41395  cdlemk55a  41396  cdleml1N  41413  cdleml3N  41415  cdlemn7  41640  cdlemn8  41641  cdlemn10  41643  dihordlem7  41651  dihordlem7b  41652  dihord1  41655  dihord10  41660  dihord11c  41661  dihord2  41664  hlhilphllem  42396  fmuldfeq  46017  seposep  49359  iscnrm3rlem8  49380  iscnrm3llem2  49383