Theorem simp3l 1199

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp13l  1286  simp23l  1292  simp33l  1298  tfisi  7680  fpr3g  8072  tfrlem5  8182  omeulem1  8375  omeulem2  8376  uniinqs  8544  elfiun  9119  tcrank  9573  isfin2-2  10006  konigthlem  10255  gruen  10499  addid2  11088  mulcan  11542  mulcan2  11543  divass  11581  divdir  11588  div11  11591  muldivdir  11598  subdivcomb1  11600  subdivcomb2  11601  divcan5  11607  ltmul1  11755  ltdiv1  11769  ltmuldiv  11778  lediv2  11795  xaddass2  12913  xlt2add  12923  xmulasslem3  12949  xadddi2  12960  expaddz  13755  expmulz  13757  muldivbinom2  13905  resqrtcl  14893  o1add  15251  o1mul  15252  o1sub  15253  dvdsadd2b  15943  dvdsgcd  16180  rpexp12i  16357  pythagtriplem3  16447  pcpremul  16472  pceu  16475  pcqmul  16482  pcqdiv  16486  setsstruct  16805  f1ocpbllem  17152  funcoppc  17506  funcres  17527  catcisolem  17741  1stfcl  17830  2ndfcl  17831  prfcl  17836  evlfcl  17856  curf1cl  17862  curfcl  17866  hofcl  17893  latjlej12  18088  latmlem12  18104  latj4  18122  latj4rot  18123  symgsssg  18990  symgfisg  18991  psgnunilem4  19020  odcong  19072  cmn4  19321  ablsub4  19329  abladdsub4  19330  lsm4  19376  abvdom  20013  abvres  20014  abvtrivd  20015  lspsolvlem  20319  lbsextlem2  20336  lidlsubcl  20400  frlmbas3  20893  matmulcell  21502  marrepeval  21620  ma1repveval  21628  submaeval  21639  mdetunilem3  21671  mdetuni0  21678  mdetmul  21680  minmar1eval  21706  nllyrest  22545  hausflimlem  23038  tsmsxp  23214  psmetlecl  23376  xmetlecl  23407  prdsxmetlem  23429  ngpocelbl  23774  bndth  24027  cph2ass  24282  iscau3  24347  dvres2  24981  coemullem  25316  vieta1  25377  aalioulem4  25400  cxpcn3lem  25805  angcan  25857  dchrvmasumlema  26553  logdivsum  26586  abvcxp  26668  padicabv  26683  ax5seglem3  27202  ax5seglem6  27205  axpasch  27212  axeuclid  27234  axcontlem4  27238  axcontlem8  27242  wlkl1loop  27907  trlsonwlkon  27979  pthontrlon  28016  wspthsswwlknon  28187  frgr2wwlkeqm  28596  adjlnop  30349  xreceu  31098  orngmul  31404  rhmdvd  31422  measvunilem  32080  measvunilem0  32081  measres  32090  bnj1128  32870  umgr2cycllem  33002  umgr2cycl  33003  satfv1fvfmla1  33285  nosupbnd1lem4  33841  nosupbnd1lem5  33842  noinfbnd1lem4  33856  cofcut1  34017  cofcut2  34018  cgrcomim  34218  cgrcoml  34225  cgrcomr  34226  cgrdegen  34233  segconeu  34240  btwnintr  34248  btwnexch3  34249  btwnouttr2  34251  btwnouttr  34253  btwnexch  34254  trisegint  34257  lineext  34305  linecgr  34310  lineid  34312  idinside  34313  btwnconn1lem3  34318  btwnconn1lem4  34319  btwnconn1lem7  34322  btwnconn1lem14  34329  btwnconn2  34331  midofsegid  34333  btwnoutside  34354  outsideoftr  34358  lineunray  34376  lineelsb2  34377  cnres2  35848  heibor  35906  lsmcv2  36970  lcvat  36971  lcvexchlem4  36978  lcvexchlem5  36979  lfladd  37007  lflsub  37008  lflmul  37009  lshpkrlem4  37054  latm4  37174  omlmod1i2N  37201  cvlatexch3  37279  cvlsupr7  37289  hlatj4  37315  hlrelat3  37353  cvrval3  37354  atcvrj1  37372  atlelt  37379  2atlt  37380  2atjm  37386  3noncolr2  37390  athgt  37397  3dimlem2  37400  3dimlem4  37405  3dimlem4OLDN  37406  3dim3  37410  1cvratex  37414  ps-1  37418  ps-2  37419  hlatexch3N  37421  llnle  37459  atcvrlln2  37460  atcvrlln  37461  lplni2  37478  lplnle  37481  lplnnle2at  37482  llncvrlpln2  37498  lplnexllnN  37505  2llnmeqat  37512  lvolnle3at  37523  4atlem0ae  37535  lplncvrlvol2  37556  lnjatN  37721  lncvrat  37723  cdlemblem  37734  elpaddri  37743  paddasslem2  37762  paddasslem16  37776  padd4N  37781  hlmod1i  37797  dalawlem2  37813  pclfinN  37841  pexmidlem4N  37914  pl42lem1N  37920  lhp2lt  37942  lhpexle1  37949  lhpexle2lem  37950  lhpj1  37963  lhpmcvr5N  37968  lhp2at0  37973  lhp2atnle  37974  lhp2at0nle  37976  lhple  37983  lhpat  37984  lhpat4N  37985  4atexlempnq  37996  4atexlem7  38016  4atex  38017  ltrn11  38067  ltrnle  38070  ltrnm  38072  ltrnj  38073  ltrncvr  38074  ltrnel  38080  ltrncnvel  38083  ltrncnv  38087  trlval2  38104  trlcnv  38106  trljat1  38107  trljat2  38108  trlat  38110  trl0  38111  trlnidat  38114  trlnid  38120  cdlemc1  38132  cdlemc2  38133  cdlemc5  38136  cdlemd2  38140  cdlemd7  38145  cdlemd8  38146  cdlemd9  38147  cdleme0e  38158  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme5  38181  cdleme10  38195  cdleme11a  38201  cdleme11c  38202  cdleme11h  38207  cdleme11j  38208  cdleme0nex  38231  cdleme18a  38232  cdleme18b  38233  cdleme22gb  38235  cdleme20zN  38242  cdleme20c  38252  cdleme20k  38260  cdleme21a  38266  cdleme21b  38267  cdleme21c  38268  cdleme21h  38275  cdleme22b  38282  cdleme22d  38284  cdleme22f  38287  cdleme25a  38294  cdleme25c  38296  cdleme25dN  38297  cdleme26ee  38301  cdleme30a  38319  cdlemefr29bpre0N  38347  cdlemefr29clN  38348  cdlemefr32fvaN  38350  cdlemefr32fva1  38351  cdlemefs29bpre0N  38357  cdlemefs29bpre1N  38358  cdlemefs29cpre1N  38359  cdlemefs29clN  38360  cdleme43fsv1snlem  38361  cdlemefs32fvaN  38363  cdlemefs32fva1  38364  cdlemefs31fv1  38365  cdleme36a  38401  cdleme39a  38406  cdleme42a  38412  cdleme42c  38413  cdleme17d3  38437  cdleme48fv  38440  cdleme48bw  38443  cdleme48b  38444  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemeg46gfv  38471  cdleme48d  38476  cdleme50trn2a  38491  cdleme50trn2  38492  cdleme50ltrn  38498  cdlemf1  38502  cdlemf  38504  trlord  38510  cdlemg2dN  38531  cdlemg2fvlem  38535  cdlemg2l  38544  cdlemg7fvbwN  38548  cdlemg7aN  38566  cdlemg10bALTN  38577  cdlemg10c  38580  cdlemg17a  38602  cdlemg17dALTN  38605  cdlemg31b0a  38636  cdlemg31a  38638  cdlemg31b  38639  cdlemg34  38653  cdlemg36  38655  ltrnco  38660  trlcoabs2N  38663  trlcolem  38667  cdlemg48  38678  tgrpov  38689  tendoco2  38709  tendoplco2  38720  cdlemh1  38756  cdlemi1  38759  cdlemi2  38760  cdlemj3  38764  tendoid0  38766  cdlemk1  38772  cdlemk2  38773  cdlemk4  38775  cdlemk8  38779  cdlemk9  38780  cdlemk9bN  38781  cdlemk10  38784  cdlemk26b-3  38846  cdlemk26-3  38847  cdlemk28-3  38849  cdlemk37  38855  cdlemk39  38857  cdlemkfid1N  38862  cdlemkid1  38863  cdlemky  38867  cdlemkyu  38868  cdlemk19ylem  38871  cdlemk19xlem  38883  cdlemk11t  38887  cdlemk51  38894  cdlemkyyN  38903  cdleml6  38922  cdleml7  38923  cdleml8  38924  cdleml9  38925  erngdvlem4  38932  erngdvlem4-rN  38940  tendospcanN  38964  dia11N  38989  cdlemm10N  39059  dib11N  39101  dicvaddcl  39131  dicvscacl  39132  cdlemn6  39143  dihvalcq2  39188  dihopelvalcpre  39189  dihord6b  39201  dihord5apre  39203  dihmeetlem1N  39231  dihmeetlem2N  39240  dihglbcpreN  39241  dihjatc1  39252  dihmeetlem20N  39267  dih1dimatlem0  39269  dihatlat  39275  dihglblem6  39281  dochexmidlem4  39404  mapdpglem32  39646  mapdh8ad  39720  mapdh9aOLDN  39731  hdmap11lem2  39783  hdmap14lem6  39814  frlmfzowrdb  40161  flt4lem5  40403  mzpsubst  40486  pellex  40573  pellfundex  40624  pellfund14gap  40625  qirropth  40646  rmxypos  40685  congmul  40705  congsub  40708  mzpcong  40710  coprmdvdsb  40723  jm2.15nn0  40741  jm2.16nn0  40742  rpnnen3lem  40769  idomsubgmo  40939  relexp01min  41210  mullimc  43047  islptre  43050  limccog  43051  mullimcf  43054  addlimc  43079  0ellimcdiv  43080  limsupre3lem  43163  stoweidlem57  43488  fourierdlem48  43585  fourierdlem80  43617  fourierdlem113  43650  ovncvrrp  43992  opnvonmbllem2  44061  ovolval5lem3  44082  ovnovollem3  44086  itsclc0lem1  45990  itsclc0lem2  45991  itschlc0yqe  45994  itscnhlc0xyqsol  45999  itschlc0xyqsol1  46000