Theorem simp32 1091

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl32  1136  simpr32  1145  simp132  1190  simp232  1199  simp332  1208  smogt  7351  axdc3lem4  9158  bitsfzo  14995  frlmphl  19939  mdetunilem4  20240  mdetuni0  20246  mdetmul  20248  decpmatmullem  20395  logfacbnd3  24748  logexprlim  24750  log2sumbnd  25033  ax5seg  25618  iocinioc2  28931  totprob  29816  cgrtr  31269  cgrtr3  31271  ofscom  31284  cgrextend  31285  segconeq  31287  ifscgr  31321  colinearxfr  31352  brofs2  31354  brifs2  31355  fscgr  31357  btwnconn1lem2  31365  btwnconn1lem9  31372  btwnconn1lem10  31373  btwnconn1lem11  31374  btwnconn1lem12  31375  brsegle2  31386  seglecgr12im  31387  seglecgr12  31388  segletr  31391  outsideofeq  31407  ivthALT  31500  lshpkrlem5  33419  lshpkrlem6  33420  atbtwnexOLDN  33751  atbtwnex  33752  4noncolr3  33757  3dimlem3a  33764  3dim1  33771  3dim2  33772  1cvrat  33780  2atjlej  33783  hlatexch4  33785  ps-2b  33786  2atm  33831  ps-2c  33832  2atmat  33865  4atlem10  33910  4atlem11b  33912  4atlem11  33913  4at  33917  4at2  33918  2lplnja  33923  2lplnj  33924  dalemswapyz  33960  dalem-ddly  33990  cdlemb  34098  paddasslem5  34128  pmodlem1  34150  dalawlem1  34175  dalawlem3  34177  dalawlem4  34178  dalawlem5  34179  dalawlem6  34180  dalawlem7  34181  dalawlem8  34182  dalawlem9  34183  dalawlem11  34185  dalawlem12  34186  dalawlem15  34189  osumcllem5N  34264  osumcllem6N  34265  lhpexle3lem  34315  lhpmcvr4N  34330  lhpmcvr6N  34332  4atexlemex6  34378  4atex2  34381  4atex2-0bOLDN  34383  4atex2-0cOLDN  34384  ltrn11at  34451  trlval3  34492  cdlemd3  34505  cdleme7aa  34547  cdleme7b  34549  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme16aN  34564  cdleme11dN  34567  cdleme11e  34568  cdleme11l  34574  cdleme11  34575  cdleme12  34576  cdleme14  34578  cdleme15a  34579  cdleme15c  34581  cdleme16c  34585  cdleme16d  34586  cdleme16e  34587  cdleme16f  34588  cdleme17c  34593  cdleme18c  34598  cdlemeda  34603  cdlemednpq  34604  cdleme19a  34609  cdleme19c  34611  cdleme20aN  34615  cdleme20bN  34616  cdleme20l1  34626  cdleme20l2  34627  cdleme22aa  34645  cdleme22a  34646  cdleme22g  34654  cdleme23b  34656  cdleme23c  34657  cdleme26fALTN  34668  cdleme26f  34669  cdleme26f2ALTN  34670  cdleme26f2  34671  cdleme28b  34677  cdleme32b  34748  cdleme32c  34749  cdleme32e  34751  cdleme35h  34762  cdleme35sn2aw  34764  cdleme38m  34769  cdleme40n  34774  cdleme41sn3aw  34780  cdleme41sn4aw  34781  cdlemeg46gfre  34838  cdlemf1  34867  cdlemg1cex  34894  cdlemg2ce  34898  cdlemg4d  34919  cdlemg4  34923  cdlemg7fvN  34930  cdlemg8b  34934  cdlemg8c  34935  cdlemg9a  34938  cdlemg11aq  34944  cdlemg10a  34946  cdlemg12a  34949  cdlemg12b  34950  cdlemg12d  34952  cdlemg12g  34955  cdlemg12  34956  cdlemg13a  34957  cdlemg13  34958  cdlemg14f  34959  cdlemg14g  34960  cdlemg17b  34968  cdlemg17dN  34969  cdlemg17e  34971  cdlemg17pq  34978  cdlemg17iqN  34980  cdlemg18c  34986  cdlemg18d  34987  cdlemg19a  34989  cdlemg19  34990  cdlemg21  34992  cdlemg27a  34998  cdlemg28a  34999  cdlemg31b0N  35000  cdlemg27b  35002  cdlemg31c  35005  cdlemg33b0  35007  cdlemg28  35010  cdlemg33a  35012  cdlemg33  35017  cdlemg35  35019  cdlemg36  35020  cdlemg44a  35037  cdlemg46  35041  cdlemh2  35122  cdlemh  35123  cdlemj1  35127  cdlemk5  35142  cdlemk6  35143  cdlemki  35147  cdlemksv2  35153  cdlemk7  35154  cdlemk11  35155  cdlemkole  35159  cdlemk14  35160  cdlemk16  35163  cdlemk1u  35165  cdlemk18  35174  cdlemk19  35175  cdlemk7u  35176  cdlemk11u  35177  cdlemk33N  35215  cdlemkid2  35230  cdlemkfid3N  35231  cdlemk11ta  35235  cdlemk11tc  35251  cdlemk45  35253  cdlemk46  35254  cdlemk47  35255  cdlemk52  35260  cdlemk53a  35261  cdlemk54  35264  cdlemk55a  35265  cdleml1N  35282  cdleml3N  35284  cdlemn7  35510  cdlemn8  35511  cdlemn10  35513  dihordlem7  35521  dihordlem7b  35522  dihord1  35525  dihord10  35530  dihord11c  35531  dihord2  35534  hlhilphllem  36269  fmuldfeq  38650