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  7795  fpr3g  8221  tfrlem5  8305  omeulem1  8503  omeulem2  8504  uniinqs  8727  elfiun  9321  tcrank  9784  isfin2-2  10217  konigthlem  10466  gruen  10710  addlid  11303  mulcan  11761  mulcan2  11762  divass  11801  divdir  11808  div11OLD  11812  muldivdir  11821  subdivcomb1  11823  subdivcomb2  11824  divcan5  11830  ltmul1  11978  ltdiv1  11993  ltmuldiv  12002  lediv2  12019  xaddass2  13151  xlt2add  13161  xmulasslem3  13187  xadddi2  13198  expaddz  14015  expmulz  14017  muldivbinom2  14172  resqrtcl  15162  o1add  15523  o1mul  15524  o1sub  15525  dvdsadd2b  16219  dvdsgcd  16457  rpexp12i  16637  pythagtriplem3  16732  pcpremul  16757  pceu  16760  pcqmul  16767  pcqdiv  16771  setsstruct  17089  f1ocpbllem  17430  funcoppc  17784  funcres  17805  catcisolem  18019  1stfcl  18105  2ndfcl  18106  prfcl  18111  evlfcl  18130  curf1cl  18136  curfcl  18140  hofcl  18167  latjlej12  18363  latmlem12  18379  latj4  18397  latj4rot  18398  symgsssg  19381  symgfisg  19382  psgnunilem4  19411  odcong  19463  cmn4  19715  ablsub4  19724  abladdsub4  19725  lsm4  19774  abvdom  20747  abvres  20748  abvtrivd  20749  orngmul  20782  lspsolvlem  21081  lbsextlem2  21098  lidlsubcl  21163  frlmbas3  21715  matmulcell  22361  marrepeval  22479  ma1repveval  22487  submaeval  22498  mdetunilem3  22530  mdetuni0  22537  mdetmul  22539  minmar1eval  22565  nllyrest  23402  hausflimlem  23895  tsmsxp  24071  psmetlecl  24231  xmetlecl  24262  prdsxmetlem  24284  ngpocelbl  24620  bndth  24885  cph2ass  25141  iscau3  25206  dvres2  25841  coemullem  26183  vieta1  26248  aalioulem4  26271  cxpcn3lem  26685  angcan  26740  dchrvmasumlema  27439  logdivsum  27472  abvcxp  27554  padicabv  27569  nosupbnd1lem4  27651  nosupbnd1lem5  27652  noinfbnd1lem4  27666  cofcut1  27865  cofcut2  27867  divsmulw  28133  precsexlem8  28153  precsexlem9  28154  ax5seglem3  28911  ax5seglem6  28914  axpasch  28921  axeuclid  28943  axcontlem4  28947  axcontlem8  28951  wlkl1loop  29618  trlsonwlkon  29688  pthontrlon  29727  wspthsswwlknon  29901  frgr2wwlkeqm  30313  adjlnop  32068  xreceu  32909  rhmdvd  33296  measvunilem  34246  measvunilem0  34247  measres  34256  bnj1128  35023  umgr2cycllem  35205  umgr2cycl  35206  satfv1fvfmla1  35488  cgrcomim  36054  cgrcoml  36061  cgrcomr  36062  cgrdegen  36069  segconeu  36076  btwnintr  36084  btwnexch3  36085  btwnouttr2  36087  btwnouttr  36089  btwnexch  36090  trisegint  36093  lineext  36141  linecgr  36146  lineid  36148  idinside  36149  btwnconn1lem3  36154  btwnconn1lem4  36155  btwnconn1lem7  36158  btwnconn1lem14  36165  btwnconn2  36167  midofsegid  36169  btwnoutside  36190  outsideoftr  36194  lineunray  36212  lineelsb2  36213  cnres2  37823  heibor  37881  lsmcv2  39148  lcvat  39149  lcvexchlem4  39156  lcvexchlem5  39157  lfladd  39185  lflsub  39186  lflmul  39187  lshpkrlem4  39232  latm4  39352  omlmod1i2N  39379  cvlatexch3  39457  cvlsupr7  39467  hlatj4  39493  hlrelat3  39531  cvrval3  39532  atcvrj1  39550  atlelt  39557  2atlt  39558  2atjm  39564  3noncolr2  39568  athgt  39575  3dimlem2  39578  3dimlem4  39583  3dimlem4OLDN  39584  3dim3  39588  1cvratex  39592  ps-1  39596  ps-2  39597  hlatexch3N  39599  llnle  39637  atcvrlln2  39638  atcvrlln  39639  lplni2  39656  lplnle  39659  lplnnle2at  39660  llncvrlpln2  39676  lplnexllnN  39683  2llnmeqat  39690  lvolnle3at  39701  4atlem0ae  39713  lplncvrlvol2  39734  lnjatN  39899  lncvrat  39901  cdlemblem  39912  elpaddri  39921  paddasslem2  39940  paddasslem16  39954  padd4N  39959  hlmod1i  39975  dalawlem2  39991  pclfinN  40019  pexmidlem4N  40092  pl42lem1N  40098  lhp2lt  40120  lhpexle1  40127  lhpexle2lem  40128  lhpj1  40141  lhpmcvr5N  40146  lhp2at0  40151  lhp2atnle  40152  lhp2at0nle  40154  lhple  40161  lhpat  40162  lhpat4N  40163  4atexlempnq  40174  4atexlem7  40194  4atex  40195  ltrn11  40245  ltrnle  40248  ltrnm  40250  ltrnj  40251  ltrncvr  40252  ltrnel  40258  ltrncnvel  40261  ltrncnv  40265  trlval2  40282  trlcnv  40284  trljat1  40285  trljat2  40286  trlat  40288  trl0  40289  trlnidat  40292  trlnid  40298  cdlemc1  40310  cdlemc2  40311  cdlemc5  40314  cdlemd2  40318  cdlemd7  40323  cdlemd8  40324  cdlemd9  40325  cdleme0e  40336  cdleme3g  40353  cdleme3h  40354  cdleme3  40356  cdleme5  40359  cdleme10  40373  cdleme11a  40379  cdleme11c  40380  cdleme11h  40385  cdleme11j  40386  cdleme0nex  40409  cdleme18a  40410  cdleme18b  40411  cdleme22gb  40413  cdleme20zN  40420  cdleme20c  40430  cdleme20k  40438  cdleme21a  40444  cdleme21b  40445  cdleme21c  40446  cdleme21h  40453  cdleme22b  40460  cdleme22d  40462  cdleme22f  40465  cdleme25a  40472  cdleme25c  40474  cdleme25dN  40475  cdleme26ee  40479  cdleme30a  40497  cdlemefr29bpre0N  40525  cdlemefr29clN  40526  cdlemefr32fvaN  40528  cdlemefr32fva1  40529  cdlemefs29bpre0N  40535  cdlemefs29bpre1N  40536  cdlemefs29cpre1N  40537  cdlemefs29clN  40538  cdleme43fsv1snlem  40539  cdlemefs32fvaN  40541  cdlemefs32fva1  40542  cdlemefs31fv1  40543  cdleme36a  40579  cdleme39a  40584  cdleme42a  40590  cdleme42c  40591  cdleme17d3  40615  cdleme48fv  40618  cdleme48bw  40621  cdleme48b  40622  cdlemeg46rgv  40647  cdlemeg46req  40648  cdlemeg46gfv  40649  cdleme48d  40654  cdleme50trn2a  40669  cdleme50trn2  40670  cdleme50ltrn  40676  cdlemf1  40680  cdlemf  40682  trlord  40688  cdlemg2dN  40709  cdlemg2fvlem  40713  cdlemg2l  40722  cdlemg7fvbwN  40726  cdlemg7aN  40744  cdlemg10bALTN  40755  cdlemg10c  40758  cdlemg17a  40780  cdlemg17dALTN  40783  cdlemg31b0a  40814  cdlemg31a  40816  cdlemg31b  40817  cdlemg34  40831  cdlemg36  40833  ltrnco  40838  trlcoabs2N  40841  trlcolem  40845  cdlemg48  40856  tgrpov  40867  tendoco2  40887  tendoplco2  40898  cdlemh1  40934  cdlemi1  40937  cdlemi2  40938  cdlemj3  40942  tendoid0  40944  cdlemk1  40950  cdlemk2  40951  cdlemk4  40953  cdlemk8  40957  cdlemk9  40958  cdlemk9bN  40959  cdlemk10  40962  cdlemk26b-3  41024  cdlemk26-3  41025  cdlemk28-3  41027  cdlemk37  41033  cdlemk39  41035  cdlemkfid1N  41040  cdlemkid1  41041  cdlemky  41045  cdlemkyu  41046  cdlemk19ylem  41049  cdlemk19xlem  41061  cdlemk11t  41065  cdlemk51  41072  cdlemkyyN  41081  cdleml6  41100  cdleml7  41101  cdleml8  41102  cdleml9  41103  erngdvlem4  41110  erngdvlem4-rN  41118  tendospcanN  41142  dia11N  41167  cdlemm10N  41237  dib11N  41279  dicvaddcl  41309  dicvscacl  41310  cdlemn6  41321  dihvalcq2  41366  dihopelvalcpre  41367  dihord6b  41379  dihord5apre  41381  dihmeetlem1N  41409  dihmeetlem2N  41418  dihglbcpreN  41419  dihjatc1  41430  dihmeetlem20N  41445  dih1dimatlem0  41447  dihatlat  41453  dihglblem6  41459  dochexmidlem4  41582  mapdpglem32  41824  mapdh8ad  41898  mapdh9aOLDN  41909  hdmap11lem2  41961  hdmap14lem6  41992  frlmfzowrdb  42622  flt4lem5  42768  mzpsubst  42865  pellex  42952  pellfundex  43003  pellfund14gap  43004  qirropth  43025  rmxypos  43064  congmul  43084  congsub  43087  mzpcong  43089  coprmdvdsb  43102  jm2.15nn0  43120  jm2.16nn0  43121  rpnnen3lem  43148  idomsubgmo  43310  relexp01min  43830  mullimc  45740  islptre  45743  limccog  45744  mullimcf  45747  addlimc  45770  0ellimcdiv  45771  limsupre3lem  45854  stoweidlem57  46179  fourierdlem48  46276  fourierdlem80  46308  fourierdlem113  46341  ovncvrrp  46686  opnvonmbllem2  46755  ovolval5lem3  46776  ovnovollem3  46780  grlimedgclnbgr  48119  itsclc0lem1  48881  itsclc0lem2  48882  itschlc0yqe  48885  itscnhlc0xyqsol  48890  itschlc0xyqsol1  48891  swapffunc  49407  fucofunc  49484  fucoppc  49535