Theorem simp33 1213

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp33	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)

Proof of Theorem simp33

Step	Hyp	Ref	Expression
1		simp3 1139	. 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:  simp133  1312  simp233  1321  simp333  1330  eqfunresadj  7316  smogt  8309  bitsfzo  16374  frlmphl  21748  mdetunilem4  22571  mdetuni0  22577  mdetmul  22579  decpmatmullem  22727  logexprlim  27204  noinfres  27702  ax5seg  29023  iocinioc2  32870  bnj966  35120  cgrtr  36208  cgrtr3  36210  ofscom  36223  segconeq  36226  btwnxfr  36272  colinearxfr  36291  fscgr  36296  btwnconn1lem1  36303  btwnconn1lem2  36304  btwnconn1lem5  36307  btwnconn1lem6  36308  btwnconn1lem8  36310  btwnconn1lem9  36311  btwnconn1lem10  36312  btwnconn1lem11  36313  btwnconn1lem12  36314  brsegle2  36325  seglecgr12im  36326  seglecgr12  36327  segletr  36330  outsideofeq  36346  lshpkrlem5  39490  lshpkrlem6  39491  atbtwnexOLDN  39823  atbtwnex  39824  4noncolr3  39829  3dimlem3a  39836  3dimlem4a  39839  3dim1  39843  3dim2  39844  1cvrat  39852  2atjlej  39855  hlatexch4  39857  ps-2b  39858  2atm  39903  ps-2c  39904  lvolex3N  39914  2atmat  39937  lvolnlelpln  39961  4atlem10  39982  4atlem11b  39984  4atlem11  39985  4at  39989  4at2  39990  2lplnja  39995  2lplnj  39996  dalemclccjdd  40064  paddasslem5  40200  paddasslem15  40210  pmodlem1  40222  dalawlem1  40247  dalawlem3  40249  dalawlem4  40250  dalawlem5  40251  dalawlem6  40252  dalawlem7  40253  dalawlem8  40254  dalawlem9  40255  dalawlem11  40257  dalawlem12  40258  dalawlem15  40261  osumcllem5N  40336  osumcllem6N  40337  lhpexle3lem  40387  lhpmcvr4N  40402  lhpmcvr6N  40404  4atexlemex6  40450  4atex2  40453  4atex2-0bOLDN  40455  4atex3  40457  ltrn11at  40523  cdlemd3  40576  cdleme7aa  40618  cdleme7b  40620  cdleme7c  40621  cdleme7d  40622  cdleme7ga  40624  cdleme16aN  40635  cdleme11dN  40638  cdleme11e  40639  cdleme11l  40645  cdleme11  40646  cdleme12  40647  cdleme14  40649  cdleme15c  40652  cdleme16b  40655  cdleme16d  40657  cdleme17b  40663  cdleme17c  40664  cdleme18c  40669  cdleme18d  40671  cdlemeda  40674  cdlemednpq  40675  cdleme19a  40679  cdleme19c  40681  cdleme20aN  40685  cdleme20bN  40686  cdleme20d  40688  cdleme20f  40690  cdleme20g  40691  cdleme20j  40694  cdleme20l1  40696  cdleme21f  40708  cdleme22aa  40715  cdleme22a  40716  cdleme22cN  40718  cdleme22e  40720  cdleme22f2  40723  cdleme22g  40724  cdleme23b  40726  cdleme23c  40727  cdleme26e  40735  cdleme26fALTN  40738  cdleme26f  40739  cdleme26f2ALTN  40740  cdleme26f2  40741  cdleme28a  40746  cdleme28b  40747  cdleme32b  40818  cdleme32c  40819  cdleme32e  40821  cdleme35h2  40833  cdleme38m  40839  cdleme41sn4aw  40851  cdlemf1  40937  cdlemg1cex  40964  cdlemg2ce  40968  cdlemg4d  40989  cdlemg4f  40991  cdlemg7fvN  41000  cdlemg8a  41003  cdlemg8b  41004  cdlemg8c  41005  cdlemg9a  41008  cdlemg11a  41013  cdlemg11aq  41014  cdlemg10a  41016  cdlemg11b  41018  cdlemg12a  41019  cdlemg12b  41020  cdlemg12d  41022  cdlemg12e  41023  cdlemg12f  41024  cdlemg12g  41025  cdlemg12  41026  cdlemg13a  41027  cdlemg13  41028  cdlemg14f  41029  cdlemg14g  41030  cdlemg17b  41038  cdlemg17dN  41039  cdlemg17e  41041  cdlemg17h  41044  cdlemg17pq  41048  cdlemg17iqN  41050  cdlemg18b  41055  cdlemg18c  41056  cdlemg18d  41057  cdlemg18  41058  cdlemg19  41060  cdlemg21  41062  cdlemg27a  41068  cdlemg31b0N  41070  cdlemg27b  41072  cdlemg33b0  41077  cdlemg33c0  41078  cdlemg28  41080  cdlemg33a  41082  cdlemg35  41089  cdlemg42  41105  cdlemg44a  41107  cdlemg47  41112  cdlemh2  41192  cdlemh  41193  cdlemj1  41197  cdlemk3  41209  cdlemk5  41212  cdlemki  41217  cdlemksv2  41223  cdlemk7  41224  cdlemk11  41225  cdlemk12  41226  cdlemkole  41229  cdlemk14  41230  cdlemk15  41231  cdlemk16a  41232  cdlemk16  41233  cdlemkj  41239  cdlemkuv2  41243  cdlemk18  41244  cdlemk19  41245  cdlemk7u  41246  cdlemk12u  41248  cdlemkoatnle-2N  41251  cdlemk13-2N  41252  cdlemkole-2N  41253  cdlemk14-2N  41254  cdlemk15-2N  41255  cdlemk16-2N  41256  cdlemk17-2N  41257  cdlemk18-2N  41262  cdlemk19-2N  41263  cdlemk7u-2N  41264  cdlemk11u-2N  41265  cdlemk12u-2N  41266  cdlemk21-2N  41267  cdlemk20-2N  41268  cdlemk22  41269  cdlemk30  41270  cdlemk31  41272  cdlemk32  41273  cdlemk24-3  41279  cdlemkid2  41300  cdlemkfid3N  41301  cdlemk45  41323  cdlemk46  41324  cdlemk47  41325  cdlemk52  41330  cdlemk53a  41331  cdleml1N  41352  cdleml3N  41354  cdlemn7  41579  cdlemn10  41582  dihordlem7  41590  dihord1  41594  dihord2a  41595  dihord10  41599  dihord11c  41600  dihord2pre2  41602  hlhilphllem  42335  fmuldfeq  45943  usgrgrtrirex  48310  grlimprclnbgredg  48357  seposep  49285  iscnrm3rlem8  49306  iscnrm3llem2  49309