Theorem simp3l 1220

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

Assertion

Ref	Expression
simp3l	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Proof of Theorem simp3l

Step	Hyp	Ref	Expression
1		simpl 488	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2ant3 1153	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp13l  1307  simp23l  1313  simp33l  1319  tfisi  7859  fpr3g  8287  tfrlem5  8371  omeulem1  8574  omeulem2  8575  uniinqs  8802  elfiun  9406  tcrank  9882  isfin2-2  10378  konigthlem  10634  gruen  10878  addlid  11474  mulcan  11934  mulcan2  11935  divass  11973  divdir  11980  muldivdir  11990  subdivcomb1  11993  subdivcomb2  11994  divcan5  12000  ltmul1  12148  ltdiv1  12162  ltmuldiv  12171  lediv2  12188  xaddass2  13361  xlt2add  13371  xmulasslem3  13397  xadddi2  13408  expaddz  14229  expmulz  14231  muldivbinom2  14387  resqrtcl  15400  o1add  15761  o1mul  15762  o1sub  15763  dvdsadd2b  16456  dvdsgcd  16697  rpexp12i  16880  pythagtriplem3  16976  pcpremul  17001  pceu  17004  pcqmul  17011  pcqdiv  17015  setsstruct  17334  f1ocpbllem  17676  funcoppc  18030  funcres  18051  catcisolem  18265  1stfcl  18351  2ndfcl  18352  prfcl  18357  evlfcl  18376  curf1cl  18382  curfcl  18386  hofcl  18413  latjlej12  18609  latmlem12  18625  latj4  18643  latj4rot  18644  symgsssg  19661  symgfisg  19662  psgnunilem4  19691  odcong  19743  cmn4  19995  ablsub4  20004  abladdsub4  20005  lsm4  20054  abvdom  21067  abvres  21068  abvtrivd  21069  orngmul  21102  lspsolvlem  21400  lbsextlem2  21417  lidlsubcl  21483  frlmbas3  22062  matmulcell  22740  marrepeval  22858  ma1repveval  22866  submaeval  22877  mdetunilem3  22909  mdetuni0  22916  mdetmul  22918  minmar1eval  22944  nllyrest  23785  hausflimlem  24278  tsmsxp  24454  psmetlecl  24614  xmetlecl  24645  prdsxmetlem  24667  ngpocelbl  25003  bndth  25259  cph2ass  25514  iscau3  25579  dvres2  26212  coemullem  26549  vieta1  26617  aalioulem4  26644  cxpcn3lem  27057  angcan  27112  dchrvmasumlema  27809  logdivsum  27842  abvcxp  27924  padicabv  27939  flt4lem5  27962  nosupbnd1lem4  28050  nosupbnd1lem5  28051  noinfbnd1lem4  28065  cofcut1  28288  cofcut2  28290  divmulsw  28561  precsexlem8  28582  precsexlem9  28583  bdayfinbndlem1  28835  ax5seglem3  29491  ax5seglem6  29494  axpasch  29501  axeuclid  29523  axcontlem4  29527  axcontlem8  29531  wlkl1loop  30200  trlsonwlkon  30274  pthontrlon  30315  wspthsswwlknon  30492  umgr2cycllem  30728  umgr2cycl  30729  frgr2wwlkeqm  30914  adjlnop  32670  xreceu  33470  rhmdvd  33867  measvunilem  34827  measvunilem0  34828  measres  34837  bnj1128  35603  satfv1fvfmla1  36157  cgrcomim  36724  cgrcoml  36731  cgrcomr  36732  cgrdegen  36739  segconeu  36746  btwnintr  36754  btwnexch3  36755  btwnouttr2  36757  btwnouttr  36759  btwnexch  36760  trisegint  36763  lineext  36811  linecgr  36816  lineid  36818  idinside  36819  btwnconn1lem3  36824  btwnconn1lem4  36825  btwnconn1lem7  36828  btwnconn1lem14  36835  btwnconn2  36837  midofsegid  36839  btwnoutside  36860  outsideoftr  36864  lineunray  36882  lineelsb2  36883  cnres2  38665  heibor  38723  lsmcv2  40054  lcvat  40055  lcvexchlem4  40062  lcvexchlem5  40063  lfladd  40091  lflsub  40092  lflmul  40093  lshpkrlem4  40138  latm4  40258  omlmod1i2N  40285  cvlatexch3  40363  cvlsupr7  40373  hlatj4  40399  hlrelat3  40437  cvrval3  40438  atcvrj1  40456  atlelt  40463  2atlt  40464  2atjm  40470  3noncolr2  40474  athgt  40481  3dimlem2  40484  3dimlem4  40489  3dimlem4OLDN  40490  3dim3  40494  1cvratex  40498  ps-1  40502  ps-2  40503  hlatexch3N  40505  llnle  40543  atcvrlln2  40544  atcvrlln  40545  lplni2  40562  lplnle  40565  lplnnle2at  40566  llncvrlpln2  40582  lplnexllnN  40589  2llnmeqat  40596  lvolnle3at  40607  4atlem0ae  40619  lplncvrlvol2  40640  lnjatN  40805  lncvrat  40807  cdlemblem  40818  elpaddri  40827  paddasslem2  40846  paddasslem16  40860  padd4N  40865  hlmod1i  40881  dalawlem2  40897  pclfinN  40925  pexmidlem4N  40998  pl42lem1N  41004  lhp2lt  41026  lhpexle1  41033  lhpexle2lem  41034  lhpj1  41047  lhpmcvr5N  41052  lhp2at0  41057  lhp2atnle  41058  lhp2at0nle  41060  lhple  41067  lhpat  41068  lhpat4N  41069  4atexlempnq  41080  4atexlem7  41100  4atex  41101  ltrn11  41151  ltrnle  41154  ltrnm  41156  ltrnj  41157  ltrncvr  41158  ltrnel  41164  ltrncnvel  41167  ltrncnv  41171  trlval2  41188  trlcnv  41190  trljat1  41191  trljat2  41192  trlat  41194  trl0  41195  trlnidat  41198  trlnid  41204  cdlemc1  41216  cdlemc2  41217  cdlemc5  41220  cdlemd2  41224  cdlemd7  41229  cdlemd8  41230  cdlemd9  41231  cdleme0e  41242  cdleme3g  41259  cdleme3h  41260  cdleme3  41262  cdleme5  41265  cdleme10  41279  cdleme11a  41285  cdleme11c  41286  cdleme11h  41291  cdleme11j  41292  cdleme0nex  41315  cdleme18a  41316  cdleme18b  41317  cdleme22gb  41319  cdleme20zN  41326  cdleme20c  41336  cdleme20k  41344  cdleme21a  41350  cdleme21b  41351  cdleme21c  41352  cdleme21h  41359  cdleme22b  41366  cdleme22d  41368  cdleme22f  41371  cdleme25a  41378  cdleme25c  41380  cdleme25dN  41381  cdleme26ee  41385  cdleme30a  41403  cdlemefr29bpre0N  41431  cdlemefr29clN  41432  cdlemefr32fvaN  41434  cdlemefr32fva1  41435  cdlemefs29bpre0N  41441  cdlemefs29bpre1N  41442  cdlemefs29cpre1N  41443  cdlemefs29clN  41444  cdleme43fsv1snlem  41445  cdlemefs32fvaN  41447  cdlemefs32fva1  41448  cdlemefs31fv1  41449  cdleme36a  41485  cdleme39a  41490  cdleme42a  41496  cdleme42c  41497  cdleme17d3  41521  cdleme48fv  41524  cdleme48bw  41527  cdleme48b  41528  cdlemeg46rgv  41553  cdlemeg46req  41554  cdlemeg46gfv  41555  cdleme48d  41560  cdleme50trn2a  41575  cdleme50trn2  41576  cdleme50ltrn  41582  cdlemf1  41586  cdlemf  41588  trlord  41594  cdlemg2dN  41615  cdlemg2fvlem  41619  cdlemg2l  41628  cdlemg7fvbwN  41632  cdlemg7aN  41650  cdlemg10bALTN  41661  cdlemg10c  41664  cdlemg17a  41686  cdlemg17dALTN  41689  cdlemg31b0a  41720  cdlemg31a  41722  cdlemg31b  41723  cdlemg34  41737  cdlemg36  41739  ltrnco  41744  trlcoabs2N  41747  trlcolem  41751  cdlemg48  41762  tgrpov  41773  tendoco2  41793  tendoplco2  41804  cdlemh1  41840  cdlemi1  41843  cdlemi2  41844  cdlemj3  41848  tendoid0  41850  cdlemk1  41856  cdlemk2  41857  cdlemk4  41859  cdlemk8  41863  cdlemk9  41864  cdlemk9bN  41865  cdlemk10  41868  cdlemk26b-3  41930  cdlemk26-3  41931  cdlemk28-3  41933  cdlemk37  41939  cdlemk39  41941  cdlemkfid1N  41946  cdlemkid1  41947  cdlemky  41951  cdlemkyu  41952  cdlemk19ylem  41955  cdlemk19xlem  41967  cdlemk11t  41971  cdlemk51  41978  cdlemkyyN  41987  cdleml6  42006  cdleml7  42007  cdleml8  42008  cdleml9  42009  erngdvlem4  42016  erngdvlem4-rN  42024  tendospcanN  42048  dia11N  42073  cdlemm10N  42143  dib11N  42185  dicvaddcl  42215  dicvscacl  42216  cdlemn6  42227  dihvalcq2  42272  dihopelvalcpre  42273  dihord6b  42285  dihord5apre  42287  dihmeetlem1N  42315  dihmeetlem2N  42324  dihglbcpreN  42325  dihjatc1  42336  dihmeetlem20N  42351  dih1dimatlem0  42353  dihatlat  42359  dihglblem6  42365  dochexmidlem4  42488  mapdpglem32  42730  mapdh8ad  42804  mapdh9aOLDN  42815  hdmap11lem2  42867  hdmap14lem6  42898  frlmfzowrdb  43536  mzpsubst  43712  pellex  43795  pellfundex  43846  pellfund14gap  43847  qirropth  43868  rmxypos  43907  congmul  43927  congsub  43930  mzpcong  43932  coprmdvdsb  43945  jm2.15nn0  43963  jm2.16nn0  43964  rpnnen3lem  43991  idomsubgmo  44153  relexp01min  44672  mullimc  46572  islptre  46575  limccog  46576  mullimcf  46579  addlimc  46602  0ellimcdiv  46603  limsupre3lem  46686  stoweidlem57  47011  fourierdlem48  47108  fourierdlem80  47140  fourierdlem113  47173  ovncvrrp  47518  opnvonmbllem2  47587  ovolval5lem3  47608  ovnovollem3  47612  grlimedgclnbgr  49037  itsclc0lem1  49812  itsclc0lem2  49813  itschlc0yqe  49816  itscnhlc0xyqsol  49821  itschlc0xyqsol1  49822  swapffunc  50334  fucofunc  50411  fucoppc  50462