Theorem simp3l 1202

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 1135	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

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

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 1088

This theorem is referenced by:  simp13l  1289  simp23l  1295  simp33l  1301  tfisi  7838  fpr3g  8267  tfrlem5  8351  omeulem1  8549  omeulem2  8550  uniinqs  8773  elfiun  9388  tcrank  9844  isfin2-2  10279  konigthlem  10528  gruen  10772  addlid  11364  mulcan  11822  mulcan2  11823  divass  11862  divdir  11869  div11OLD  11873  muldivdir  11882  subdivcomb1  11884  subdivcomb2  11885  divcan5  11891  ltmul1  12039  ltdiv1  12054  ltmuldiv  12063  lediv2  12080  xaddass2  13217  xlt2add  13227  xmulasslem3  13253  xadddi2  13264  expaddz  14078  expmulz  14080  muldivbinom2  14235  resqrtcl  15226  o1add  15587  o1mul  15588  o1sub  15589  dvdsadd2b  16283  dvdsgcd  16521  rpexp12i  16701  pythagtriplem3  16796  pcpremul  16821  pceu  16824  pcqmul  16831  pcqdiv  16835  setsstruct  17153  f1ocpbllem  17494  funcoppc  17844  funcres  17865  catcisolem  18079  1stfcl  18165  2ndfcl  18166  prfcl  18171  evlfcl  18190  curf1cl  18196  curfcl  18200  hofcl  18227  latjlej12  18421  latmlem12  18437  latj4  18455  latj4rot  18456  symgsssg  19404  symgfisg  19405  psgnunilem4  19434  odcong  19486  cmn4  19738  ablsub4  19747  abladdsub4  19748  lsm4  19797  abvdom  20746  abvres  20747  abvtrivd  20748  lspsolvlem  21059  lbsextlem2  21076  lidlsubcl  21141  frlmbas3  21692  matmulcell  22339  marrepeval  22457  ma1repveval  22465  submaeval  22476  mdetunilem3  22508  mdetuni0  22515  mdetmul  22517  minmar1eval  22543  nllyrest  23380  hausflimlem  23873  tsmsxp  24049  psmetlecl  24210  xmetlecl  24241  prdsxmetlem  24263  ngpocelbl  24599  bndth  24864  cph2ass  25120  iscau3  25185  dvres2  25820  coemullem  26162  vieta1  26227  aalioulem4  26250  cxpcn3lem  26664  angcan  26719  dchrvmasumlema  27418  logdivsum  27451  abvcxp  27533  padicabv  27548  nosupbnd1lem4  27630  nosupbnd1lem5  27631  noinfbnd1lem4  27645  cofcut1  27835  cofcut2  27837  divsmulw  28103  precsexlem8  28123  precsexlem9  28124  ax5seglem3  28865  ax5seglem6  28868  axpasch  28875  axeuclid  28897  axcontlem4  28901  axcontlem8  28905  wlkl1loop  29573  trlsonwlkon  29645  pthontrlon  29684  wspthsswwlknon  29858  frgr2wwlkeqm  30267  adjlnop  32022  xreceu  32849  orngmul  33288  rhmdvd  33303  measvunilem  34209  measvunilem0  34210  measres  34219  bnj1128  34987  umgr2cycllem  35134  umgr2cycl  35135  satfv1fvfmla1  35417  cgrcomim  35984  cgrcoml  35991  cgrcomr  35992  cgrdegen  35999  segconeu  36006  btwnintr  36014  btwnexch3  36015  btwnouttr2  36017  btwnouttr  36019  btwnexch  36020  trisegint  36023  lineext  36071  linecgr  36076  lineid  36078  idinside  36079  btwnconn1lem3  36084  btwnconn1lem4  36085  btwnconn1lem7  36088  btwnconn1lem14  36095  btwnconn2  36097  midofsegid  36099  btwnoutside  36120  outsideoftr  36124  lineunray  36142  lineelsb2  36143  cnres2  37764  heibor  37822  lsmcv2  39029  lcvat  39030  lcvexchlem4  39037  lcvexchlem5  39038  lfladd  39066  lflsub  39067  lflmul  39068  lshpkrlem4  39113  latm4  39233  omlmod1i2N  39260  cvlatexch3  39338  cvlsupr7  39348  hlatj4  39374  hlrelat3  39413  cvrval3  39414  atcvrj1  39432  atlelt  39439  2atlt  39440  2atjm  39446  3noncolr2  39450  athgt  39457  3dimlem2  39460  3dimlem4  39465  3dimlem4OLDN  39466  3dim3  39470  1cvratex  39474  ps-1  39478  ps-2  39479  hlatexch3N  39481  llnle  39519  atcvrlln2  39520  atcvrlln  39521  lplni2  39538  lplnle  39541  lplnnle2at  39542  llncvrlpln2  39558  lplnexllnN  39565  2llnmeqat  39572  lvolnle3at  39583  4atlem0ae  39595  lplncvrlvol2  39616  lnjatN  39781  lncvrat  39783  cdlemblem  39794  elpaddri  39803  paddasslem2  39822  paddasslem16  39836  padd4N  39841  hlmod1i  39857  dalawlem2  39873  pclfinN  39901  pexmidlem4N  39974  pl42lem1N  39980  lhp2lt  40002  lhpexle1  40009  lhpexle2lem  40010  lhpj1  40023  lhpmcvr5N  40028  lhp2at0  40033  lhp2atnle  40034  lhp2at0nle  40036  lhple  40043  lhpat  40044  lhpat4N  40045  4atexlempnq  40056  4atexlem7  40076  4atex  40077  ltrn11  40127  ltrnle  40130  ltrnm  40132  ltrnj  40133  ltrncvr  40134  ltrnel  40140  ltrncnvel  40143  ltrncnv  40147  trlval2  40164  trlcnv  40166  trljat1  40167  trljat2  40168  trlat  40170  trl0  40171  trlnidat  40174  trlnid  40180  cdlemc1  40192  cdlemc2  40193  cdlemc5  40196  cdlemd2  40200  cdlemd7  40205  cdlemd8  40206  cdlemd9  40207  cdleme0e  40218  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme5  40241  cdleme10  40255  cdleme11a  40261  cdleme11c  40262  cdleme11h  40267  cdleme11j  40268  cdleme0nex  40291  cdleme18a  40292  cdleme18b  40293  cdleme22gb  40295  cdleme20zN  40302  cdleme20c  40312  cdleme20k  40320  cdleme21a  40326  cdleme21b  40327  cdleme21c  40328  cdleme21h  40335  cdleme22b  40342  cdleme22d  40344  cdleme22f  40347  cdleme25a  40354  cdleme25c  40356  cdleme25dN  40357  cdleme26ee  40361  cdleme30a  40379  cdlemefr29bpre0N  40407  cdlemefr29clN  40408  cdlemefr32fvaN  40410  cdlemefr32fva1  40411  cdlemefs29bpre0N  40417  cdlemefs29bpre1N  40418  cdlemefs29cpre1N  40419  cdlemefs29clN  40420  cdleme43fsv1snlem  40421  cdlemefs32fvaN  40423  cdlemefs32fva1  40424  cdlemefs31fv1  40425  cdleme36a  40461  cdleme39a  40466  cdleme42a  40472  cdleme42c  40473  cdleme17d3  40497  cdleme48fv  40500  cdleme48bw  40503  cdleme48b  40504  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemeg46gfv  40531  cdleme48d  40536  cdleme50trn2a  40551  cdleme50trn2  40552  cdleme50ltrn  40558  cdlemf1  40562  cdlemf  40564  trlord  40570  cdlemg2dN  40591  cdlemg2fvlem  40595  cdlemg2l  40604  cdlemg7fvbwN  40608  cdlemg7aN  40626  cdlemg10bALTN  40637  cdlemg10c  40640  cdlemg17a  40662  cdlemg17dALTN  40665  cdlemg31b0a  40696  cdlemg31a  40698  cdlemg31b  40699  cdlemg34  40713  cdlemg36  40715  ltrnco  40720  trlcoabs2N  40723  trlcolem  40727  cdlemg48  40738  tgrpov  40749  tendoco2  40769  tendoplco2  40780  cdlemh1  40816  cdlemi1  40819  cdlemi2  40820  cdlemj3  40824  tendoid0  40826  cdlemk1  40832  cdlemk2  40833  cdlemk4  40835  cdlemk8  40839  cdlemk9  40840  cdlemk9bN  40841  cdlemk10  40844  cdlemk26b-3  40906  cdlemk26-3  40907  cdlemk28-3  40909  cdlemk37  40915  cdlemk39  40917  cdlemkfid1N  40922  cdlemkid1  40923  cdlemky  40927  cdlemkyu  40928  cdlemk19ylem  40931  cdlemk19xlem  40943  cdlemk11t  40947  cdlemk51  40954  cdlemkyyN  40963  cdleml6  40982  cdleml7  40983  cdleml8  40984  cdleml9  40985  erngdvlem4  40992  erngdvlem4-rN  41000  tendospcanN  41024  dia11N  41049  cdlemm10N  41119  dib11N  41161  dicvaddcl  41191  dicvscacl  41192  cdlemn6  41203  dihvalcq2  41248  dihopelvalcpre  41249  dihord6b  41261  dihord5apre  41263  dihmeetlem1N  41291  dihmeetlem2N  41300  dihglbcpreN  41301  dihjatc1  41312  dihmeetlem20N  41327  dih1dimatlem0  41329  dihatlat  41335  dihglblem6  41341  dochexmidlem4  41464  mapdpglem32  41706  mapdh8ad  41780  mapdh9aOLDN  41791  hdmap11lem2  41843  hdmap14lem6  41874  frlmfzowrdb  42499  flt4lem5  42645  mzpsubst  42743  pellex  42830  pellfundex  42881  pellfund14gap  42882  qirropth  42903  rmxypos  42943  congmul  42963  congsub  42966  mzpcong  42968  coprmdvdsb  42981  jm2.15nn0  42999  jm2.16nn0  43000  rpnnen3lem  43027  idomsubgmo  43189  relexp01min  43709  mullimc  45621  islptre  45624  limccog  45625  mullimcf  45628  addlimc  45653  0ellimcdiv  45654  limsupre3lem  45737  stoweidlem57  46062  fourierdlem48  46159  fourierdlem80  46191  fourierdlem113  46224  ovncvrrp  46569  opnvonmbllem2  46638  ovolval5lem3  46659  ovnovollem3  46663  itsclc0lem1  48749  itsclc0lem2  48750  itschlc0yqe  48753  itscnhlc0xyqsol  48758  itschlc0xyqsol1  48759  swapffunc  49275  fucofunc  49352  fucoppc  49403