Theorem simp31 1226

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

Assertion

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

Proof of Theorem simp31

Step	Hyp	Ref	Expression
1		simp1 1152	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜒)
2	1	3ad2ant3 1151	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simp131  1325  simp231  1334  simp331  1343  eqfunresadj  7356  smogt  8350  frlmphl  21896  mdetuni0  22743  mdetmul  22745  gsummatr01lem3  22779  decpmatmullem  22893  tsmsxp  24277  log2sumbnd  27670  nosupres  27833  noinfres  27848  ax5seg  29225  wlkoniswlk  29946  iocinioc2  33061  totprob  34758  cgrtr  36379  cgrtr3  36381  ofscom  36394  cgrextend  36395  segconeq  36397  ifscgr  36431  btwnxfr  36443  colinearxfr  36462  brofs2  36464  brifs2  36465  fscgr  36467  btwnconn1lem1  36474  btwnconn1lem2  36475  btwnconn1lem5  36478  btwnconn1lem6  36479  btwnconn1lem7  36480  btwnconn1lem8  36481  btwnconn1lem9  36482  btwnconn1lem10  36483  btwnconn1lem11  36484  btwnconn1lem12  36485  seglecgr12im  36497  seglecgr12  36498  segletr  36501  outsideofeq  36517  ivthALT  36731  lshpkrlem5  39773  lshpkrlem6  39774  exatleN  40063  atbtwn  40105  atbtwnexOLDN  40106  atbtwnex  40107  4noncolr3  40112  3dimlem3a  40119  3dimlem4a  40122  3dim1  40126  3dim2  40127  1cvrat  40135  2atjlej  40138  hlatexch4  40140  ps-2b  40141  2atm  40186  2atmat  40220  4atlem11b  40267  4atlem11  40268  4at  40272  4at2  40273  2lplnja  40278  2lplnj  40279  dalemswapyz  40315  dalemccnedd  40346  cdlemb  40453  paddasslem5  40483  paddasslem15  40493  pmodlem1  40505  dalawlem1  40530  dalawlem3  40532  dalawlem4  40533  dalawlem5  40534  dalawlem6  40535  dalawlem7  40536  dalawlem8  40537  dalawlem9  40538  dalawlem11  40540  dalawlem12  40541  dalawlem15  40544  osumcllem5N  40619  osumcllem6N  40620  lhpexle3lem  40670  lhpmcvr4N  40685  lhpmcvr6N  40687  4atex2  40736  4atex2-0bOLDN  40738  4atex3  40740  ltrn11at  40806  trlval3  40846  cdlemd3  40859  cdleme0moN  40884  cdleme7aa  40901  cdleme7b  40903  cdleme7c  40904  cdleme7d  40905  cdleme7e  40906  cdleme7ga  40907  cdleme7  40908  cdleme16aN  40918  cdleme11dN  40921  cdleme11e  40922  cdleme11l  40928  cdleme11  40929  cdleme12  40930  cdleme14  40932  cdleme15b  40934  cdleme15c  40935  cdleme16b  40938  cdleme16c  40939  cdleme16d  40940  cdleme16e  40941  cdleme16f  40942  cdleme17c  40947  cdleme18c  40952  cdleme18d  40954  cdlemeda  40957  cdleme19a  40962  cdleme19b  40963  cdleme19c  40964  cdleme20aN  40968  cdleme20bN  40969  cdleme20d  40971  cdleme20i  40976  cdleme20j  40977  cdleme20l1  40979  cdleme20l2  40980  cdleme21d  40989  cdleme21e  40990  cdleme21f  40991  cdleme22aa  40998  cdleme22e  41003  cdleme22eALTN  41004  cdleme22f2  41006  cdleme22g  41007  cdleme23b  41009  cdleme26eALTN  41020  cdleme26fALTN  41021  cdleme26f  41022  cdleme26f2ALTN  41023  cdleme26f2  41024  cdleme28a  41029  cdleme28b  41030  cdleme32b  41101  cdleme32c  41102  cdleme32e  41104  cdleme35h  41115  cdleme35sn2aw  41117  cdleme41sn3aw  41133  cdleme41sn4aw  41134  cdlemeg46gfre  41191  cdlemf1  41220  cdlemg1cex  41247  cdlemg2ce  41251  cdlemg4d  41272  cdlemg4e  41273  cdlemg4f  41274  cdlemg4  41276  cdlemg6d  41280  cdlemg6e  41281  cdlemg7fvN  41283  cdlemg8b  41287  cdlemg8c  41288  cdlemg9a  41291  cdlemg9b  41292  cdlemg9  41293  cdlemg11aq  41297  cdlemg10a  41299  cdlemg12a  41302  cdlemg12b  41303  cdlemg12c  41304  cdlemg12d  41305  cdlemg13  41311  cdlemg14f  41312  cdlemg14g  41313  cdlemg17b  41321  cdlemg17dN  41322  cdlemg17e  41324  cdlemg17i  41328  cdlemg17pq  41331  cdlemg17iqN  41333  cdlemg18c  41339  cdlemg18d  41340  cdlemg18  41341  cdlemg19  41343  cdlemg21  41345  cdlemg27a  41351  cdlemg31b0N  41353  cdlemg27b  41355  cdlemg31c  41358  cdlemg33b0  41360  cdlemg33c0  41361  cdlemg33  41370  cdlemg35  41372  cdlemg43  41389  cdlemg44a  41390  cdlemg46  41394  cdlemh2  41475  cdlemh  41476  cdlemj1  41480  cdlemk3  41492  cdlemk5  41495  cdlemk6  41496  cdlemki  41500  cdlemksv2  41506  cdlemk12  41509  cdlemk15  41514  cdlemk16  41516  cdlemk18  41527  cdlemk19  41528  cdlemk7u  41529  cdlemk12u  41531  cdlemkoatnle-2N  41534  cdlemk13-2N  41535  cdlemkole-2N  41536  cdlemk14-2N  41537  cdlemk15-2N  41538  cdlemk16-2N  41539  cdlemk17-2N  41540  cdlemk18-2N  41545  cdlemk19-2N  41546  cdlemk7u-2N  41547  cdlemk11u-2N  41548  cdlemk12u-2N  41549  cdlemk20-2N  41551  cdlemk22  41552  cdlemk30  41553  cdlemk31  41555  cdlemk24-3  41562  cdlemkid2  41583  cdlemkfid3N  41584  cdlemk11ta  41588  cdlemkid3N  41592  cdlemk11tc  41604  cdlemk45  41606  cdlemk46  41607  cdlemk47  41608  cdlemk52  41613  cdlemk53a  41614  cdlemk53b  41615  cdleml1N  41635  cdleml3N  41637  cdlemn7  41862  cdlemn10  41865  dihordlem7  41873  dihord1  41877  dihord11c  41883  dihord2  41886  hlhilphllem  42618  fmuldfeq  46186  seposep  49584  iscnrm3rlem8  49605  iscnrm3llem2  49608