Theorem simp3l 1218

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ 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:  simp13l  1305  simp23l  1311  simp33l  1317  tfisi  7843  fpr3g  8270  tfrlem5  8354  omeulem1  8555  omeulem2  8556  uniinqs  8783  elfiun  9378  tcrank  9844  isfin2-2  10291  konigthlem  10541  gruen  10785  addlid  11381  mulcan  11839  mulcan2  11840  divass  11878  divdir  11885  muldivdir  11895  subdivcomb1  11898  subdivcomb2  11899  divcan5  11905  ltmul1  12053  ltdiv1  12067  ltmuldiv  12076  lediv2  12093  xaddass2  13264  xlt2add  13274  xmulasslem3  13300  xadddi2  13311  expaddz  14130  expmulz  14132  muldivbinom2  14287  resqrtcl  15292  o1add  15653  o1mul  15654  o1sub  15655  dvdsadd2b  16352  dvdsgcd  16590  rpexp12i  16771  pythagtriplem3  16866  pcpremul  16891  pceu  16894  pcqmul  16901  pcqdiv  16905  setsstruct  17224  f1ocpbllem  17566  funcoppc  17920  funcres  17941  catcisolem  18155  1stfcl  18241  2ndfcl  18242  prfcl  18247  evlfcl  18266  curf1cl  18272  curfcl  18276  hofcl  18303  latjlej12  18499  latmlem12  18515  latj4  18533  latj4rot  18534  symgsssg  19525  symgfisg  19526  psgnunilem4  19555  odcong  19607  cmn4  19859  ablsub4  19868  abladdsub4  19869  lsm4  19918  abvdom  20899  abvres  20900  abvtrivd  20901  orngmul  20934  lspsolvlem  21232  lbsextlem2  21249  lidlsubcl  21315  frlmbas3  21883  matmulcell  22559  marrepeval  22677  ma1repveval  22685  submaeval  22696  mdetunilem3  22728  mdetuni0  22735  mdetmul  22737  minmar1eval  22763  nllyrest  23600  hausflimlem  24093  tsmsxp  24269  psmetlecl  24429  xmetlecl  24460  prdsxmetlem  24482  ngpocelbl  24818  bndth  25074  cph2ass  25329  iscau3  25394  dvres2  26028  coemullem  26364  vieta1  26430  aalioulem4  26453  cxpcn3lem  26866  angcan  26921  dchrvmasumlema  27618  logdivsum  27651  abvcxp  27733  padicabv  27748  nosupbnd1lem4  27829  nosupbnd1lem5  27830  noinfbnd1lem4  27844  cofcut1  28067  cofcut2  28069  divmulsw  28340  precsexlem8  28361  precsexlem9  28362  bdayfinbndlem1  28614  ax5seglem3  29186  ax5seglem6  29189  axpasch  29196  axeuclid  29218  axcontlem4  29222  axcontlem8  29226  wlkl1loop  29892  trlsonwlkon  29962  pthontrlon  30001  wspthsswwlknon  30175  frgr2wwlkeqm  30587  adjlnop  32343  xreceu  33149  rhmdvd  33554  measvunilem  34514  measvunilem0  34515  measres  34524  bnj1128  35290  umgr2cycllem  35498  umgr2cycl  35499  satfv1fvfmla1  35781  cgrcomim  36347  cgrcoml  36354  cgrcomr  36355  cgrdegen  36362  segconeu  36369  btwnintr  36377  btwnexch3  36378  btwnouttr2  36380  btwnouttr  36382  btwnexch  36383  trisegint  36386  lineext  36434  linecgr  36439  lineid  36441  idinside  36442  btwnconn1lem3  36447  btwnconn1lem4  36448  btwnconn1lem7  36451  btwnconn1lem14  36458  btwnconn2  36460  midofsegid  36462  btwnoutside  36483  outsideoftr  36487  lineunray  36505  lineelsb2  36506  cnres2  38269  heibor  38327  lsmcv2  39660  lcvat  39661  lcvexchlem4  39668  lcvexchlem5  39669  lfladd  39697  lflsub  39698  lflmul  39699  lshpkrlem4  39744  latm4  39864  omlmod1i2N  39891  cvlatexch3  39969  cvlsupr7  39979  hlatj4  40005  hlrelat3  40043  cvrval3  40044  atcvrj1  40062  atlelt  40069  2atlt  40070  2atjm  40076  3noncolr2  40080  athgt  40087  3dimlem2  40090  3dimlem4  40095  3dimlem4OLDN  40096  3dim3  40100  1cvratex  40104  ps-1  40108  ps-2  40109  hlatexch3N  40111  llnle  40149  atcvrlln2  40150  atcvrlln  40151  lplni2  40168  lplnle  40171  lplnnle2at  40172  llncvrlpln2  40188  lplnexllnN  40195  2llnmeqat  40202  lvolnle3at  40213  4atlem0ae  40225  lplncvrlvol2  40246  lnjatN  40411  lncvrat  40413  cdlemblem  40424  elpaddri  40433  paddasslem2  40452  paddasslem16  40466  padd4N  40471  hlmod1i  40487  dalawlem2  40503  pclfinN  40531  pexmidlem4N  40604  pl42lem1N  40610  lhp2lt  40632  lhpexle1  40639  lhpexle2lem  40640  lhpj1  40653  lhpmcvr5N  40658  lhp2at0  40663  lhp2atnle  40664  lhp2at0nle  40666  lhple  40673  lhpat  40674  lhpat4N  40675  4atexlempnq  40686  4atexlem7  40706  4atex  40707  ltrn11  40757  ltrnle  40760  ltrnm  40762  ltrnj  40763  ltrncvr  40764  ltrnel  40770  ltrncnvel  40773  ltrncnv  40777  trlval2  40794  trlcnv  40796  trljat1  40797  trljat2  40798  trlat  40800  trl0  40801  trlnidat  40804  trlnid  40810  cdlemc1  40822  cdlemc2  40823  cdlemc5  40826  cdlemd2  40830  cdlemd7  40835  cdlemd8  40836  cdlemd9  40837  cdleme0e  40848  cdleme3g  40865  cdleme3h  40866  cdleme3  40868  cdleme5  40871  cdleme10  40885  cdleme11a  40891  cdleme11c  40892  cdleme11h  40897  cdleme11j  40898  cdleme0nex  40921  cdleme18a  40922  cdleme18b  40923  cdleme22gb  40925  cdleme20zN  40932  cdleme20c  40942  cdleme20k  40950  cdleme21a  40956  cdleme21b  40957  cdleme21c  40958  cdleme21h  40965  cdleme22b  40972  cdleme22d  40974  cdleme22f  40977  cdleme25a  40984  cdleme25c  40986  cdleme25dN  40987  cdleme26ee  40991  cdleme30a  41009  cdlemefr29bpre0N  41037  cdlemefr29clN  41038  cdlemefr32fvaN  41040  cdlemefr32fva1  41041  cdlemefs29bpre0N  41047  cdlemefs29bpre1N  41048  cdlemefs29cpre1N  41049  cdlemefs29clN  41050  cdleme43fsv1snlem  41051  cdlemefs32fvaN  41053  cdlemefs32fva1  41054  cdlemefs31fv1  41055  cdleme36a  41091  cdleme39a  41096  cdleme42a  41102  cdleme42c  41103  cdleme17d3  41127  cdleme48fv  41130  cdleme48bw  41133  cdleme48b  41134  cdlemeg46rgv  41159  cdlemeg46req  41160  cdlemeg46gfv  41161  cdleme48d  41166  cdleme50trn2a  41181  cdleme50trn2  41182  cdleme50ltrn  41188  cdlemf1  41192  cdlemf  41194  trlord  41200  cdlemg2dN  41221  cdlemg2fvlem  41225  cdlemg2l  41234  cdlemg7fvbwN  41238  cdlemg7aN  41256  cdlemg10bALTN  41267  cdlemg10c  41270  cdlemg17a  41292  cdlemg17dALTN  41295  cdlemg31b0a  41326  cdlemg31a  41328  cdlemg31b  41329  cdlemg34  41343  cdlemg36  41345  ltrnco  41350  trlcoabs2N  41353  trlcolem  41357  cdlemg48  41368  tgrpov  41379  tendoco2  41399  tendoplco2  41410  cdlemh1  41446  cdlemi1  41449  cdlemi2  41450  cdlemj3  41454  tendoid0  41456  cdlemk1  41462  cdlemk2  41463  cdlemk4  41465  cdlemk8  41469  cdlemk9  41470  cdlemk9bN  41471  cdlemk10  41474  cdlemk26b-3  41536  cdlemk26-3  41537  cdlemk28-3  41539  cdlemk37  41545  cdlemk39  41547  cdlemkfid1N  41552  cdlemkid1  41553  cdlemky  41557  cdlemkyu  41558  cdlemk19ylem  41561  cdlemk19xlem  41573  cdlemk11t  41577  cdlemk51  41584  cdlemkyyN  41593  cdleml6  41612  cdleml7  41613  cdleml8  41614  cdleml9  41615  erngdvlem4  41622  erngdvlem4-rN  41630  tendospcanN  41654  dia11N  41679  cdlemm10N  41749  dib11N  41791  dicvaddcl  41821  dicvscacl  41822  cdlemn6  41833  dihvalcq2  41878  dihopelvalcpre  41879  dihord6b  41891  dihord5apre  41893  dihmeetlem1N  41921  dihmeetlem2N  41930  dihglbcpreN  41931  dihjatc1  41942  dihmeetlem20N  41957  dih1dimatlem0  41959  dihatlat  41965  dihglblem6  41971  dochexmidlem4  42094  mapdpglem32  42336  mapdh8ad  42410  mapdh9aOLDN  42421  hdmap11lem2  42473  hdmap14lem6  42504  frlmfzowrdb  43133  flt4lem5  43239  mzpsubst  43336  pellex  43419  pellfundex  43470  pellfund14gap  43471  qirropth  43492  rmxypos  43531  congmul  43551  congsub  43554  mzpcong  43556  coprmdvdsb  43569  jm2.15nn0  43587  jm2.16nn0  43588  rpnnen3lem  43615  idomsubgmo  43777  relexp01min  44296  mullimc  46191  islptre  46194  limccog  46195  mullimcf  46198  addlimc  46221  0ellimcdiv  46222  limsupre3lem  46305  stoweidlem57  46630  fourierdlem48  46727  fourierdlem80  46759  fourierdlem113  46792  ovncvrrp  47137  opnvonmbllem2  47206  ovolval5lem3  47227  ovnovollem3  47231  grlimedgclnbgr  48616  itsclc0lem1  49388  itsclc0lem2  49389  itschlc0yqe  49392  itscnhlc0xyqsol  49397  itschlc0xyqsol1  49398  swapffunc  49912  fucofunc  49989  fucoppc  50040