Theorem simp3l 1201

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 1087

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 1089

This theorem is referenced by:  simp13l  1288  simp23l  1294  simp33l  1300  tfisi  7896  fpr3g  8326  tfrlem5  8436  omeulem1  8638  omeulem2  8639  uniinqs  8855  elfiun  9499  tcrank  9953  isfin2-2  10388  konigthlem  10637  gruen  10881  addlid  11473  mulcan  11927  mulcan2  11928  divass  11967  divdir  11974  div11OLD  11978  muldivdir  11987  subdivcomb1  11989  subdivcomb2  11990  divcan5  11996  ltmul1  12144  ltdiv1  12159  ltmuldiv  12168  lediv2  12185  xaddass2  13312  xlt2add  13322  xmulasslem3  13348  xadddi2  13359  expaddz  14157  expmulz  14159  muldivbinom2  14312  resqrtcl  15302  o1add  15660  o1mul  15661  o1sub  15662  dvdsadd2b  16354  dvdsgcd  16591  rpexp12i  16771  pythagtriplem3  16865  pcpremul  16890  pceu  16893  pcqmul  16900  pcqdiv  16904  setsstruct  17223  f1ocpbllem  17584  funcoppc  17939  funcres  17960  catcisolem  18177  1stfcl  18266  2ndfcl  18267  prfcl  18272  evlfcl  18292  curf1cl  18298  curfcl  18302  hofcl  18329  latjlej12  18525  latmlem12  18541  latj4  18559  latj4rot  18560  symgsssg  19509  symgfisg  19510  psgnunilem4  19539  odcong  19591  cmn4  19843  ablsub4  19852  abladdsub4  19853  lsm4  19902  abvdom  20853  abvres  20854  abvtrivd  20855  lspsolvlem  21167  lbsextlem2  21184  lidlsubcl  21257  frlmbas3  21819  matmulcell  22472  marrepeval  22590  ma1repveval  22598  submaeval  22609  mdetunilem3  22641  mdetuni0  22648  mdetmul  22650  minmar1eval  22676  nllyrest  23515  hausflimlem  24008  tsmsxp  24184  psmetlecl  24346  xmetlecl  24377  prdsxmetlem  24399  ngpocelbl  24746  bndth  25009  cph2ass  25266  iscau3  25331  dvres2  25967  coemullem  26309  vieta1  26372  aalioulem4  26395  cxpcn3lem  26808  angcan  26863  dchrvmasumlema  27562  logdivsum  27595  abvcxp  27677  padicabv  27692  nosupbnd1lem4  27774  nosupbnd1lem5  27775  noinfbnd1lem4  27789  cofcut1  27972  cofcut2  27974  divsmulw  28236  precsexlem8  28256  precsexlem9  28257  ax5seglem3  28964  ax5seglem6  28967  axpasch  28974  axeuclid  28996  axcontlem4  29000  axcontlem8  29004  wlkl1loop  29674  trlsonwlkon  29746  pthontrlon  29783  wspthsswwlknon  29954  frgr2wwlkeqm  30363  adjlnop  32118  xreceu  32886  orngmul  33298  rhmdvd  33313  measvunilem  34176  measvunilem0  34177  measres  34186  bnj1128  34966  umgr2cycllem  35108  umgr2cycl  35109  satfv1fvfmla1  35391  cgrcomim  35953  cgrcoml  35960  cgrcomr  35961  cgrdegen  35968  segconeu  35975  btwnintr  35983  btwnexch3  35984  btwnouttr2  35986  btwnouttr  35988  btwnexch  35989  trisegint  35992  lineext  36040  linecgr  36045  lineid  36047  idinside  36048  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem7  36057  btwnconn1lem14  36064  btwnconn2  36066  midofsegid  36068  btwnoutside  36089  outsideoftr  36093  lineunray  36111  lineelsb2  36112  cnres2  37723  heibor  37781  lsmcv2  38985  lcvat  38986  lcvexchlem4  38993  lcvexchlem5  38994  lfladd  39022  lflsub  39023  lflmul  39024  lshpkrlem4  39069  latm4  39189  omlmod1i2N  39216  cvlatexch3  39294  cvlsupr7  39304  hlatj4  39330  hlrelat3  39369  cvrval3  39370  atcvrj1  39388  atlelt  39395  2atlt  39396  2atjm  39402  3noncolr2  39406  athgt  39413  3dimlem2  39416  3dimlem4  39421  3dimlem4OLDN  39422  3dim3  39426  1cvratex  39430  ps-1  39434  ps-2  39435  hlatexch3N  39437  llnle  39475  atcvrlln2  39476  atcvrlln  39477  lplni2  39494  lplnle  39497  lplnnle2at  39498  llncvrlpln2  39514  lplnexllnN  39521  2llnmeqat  39528  lvolnle3at  39539  4atlem0ae  39551  lplncvrlvol2  39572  lnjatN  39737  lncvrat  39739  cdlemblem  39750  elpaddri  39759  paddasslem2  39778  paddasslem16  39792  padd4N  39797  hlmod1i  39813  dalawlem2  39829  pclfinN  39857  pexmidlem4N  39930  pl42lem1N  39936  lhp2lt  39958  lhpexle1  39965  lhpexle2lem  39966  lhpj1  39979  lhpmcvr5N  39984  lhp2at0  39989  lhp2atnle  39990  lhp2at0nle  39992  lhple  39999  lhpat  40000  lhpat4N  40001  4atexlempnq  40012  4atexlem7  40032  4atex  40033  ltrn11  40083  ltrnle  40086  ltrnm  40088  ltrnj  40089  ltrncvr  40090  ltrnel  40096  ltrncnvel  40099  ltrncnv  40103  trlval2  40120  trlcnv  40122  trljat1  40123  trljat2  40124  trlat  40126  trl0  40127  trlnidat  40130  trlnid  40136  cdlemc1  40148  cdlemc2  40149  cdlemc5  40152  cdlemd2  40156  cdlemd7  40161  cdlemd8  40162  cdlemd9  40163  cdleme0e  40174  cdleme3g  40191  cdleme3h  40192  cdleme3  40194  cdleme5  40197  cdleme10  40211  cdleme11a  40217  cdleme11c  40218  cdleme11h  40223  cdleme11j  40224  cdleme0nex  40247  cdleme18a  40248  cdleme18b  40249  cdleme22gb  40251  cdleme20zN  40258  cdleme20c  40268  cdleme20k  40276  cdleme21a  40282  cdleme21b  40283  cdleme21c  40284  cdleme21h  40291  cdleme22b  40298  cdleme22d  40300  cdleme22f  40303  cdleme25a  40310  cdleme25c  40312  cdleme25dN  40313  cdleme26ee  40317  cdleme30a  40335  cdlemefr29bpre0N  40363  cdlemefr29clN  40364  cdlemefr32fvaN  40366  cdlemefr32fva1  40367  cdlemefs29bpre0N  40373  cdlemefs29bpre1N  40374  cdlemefs29cpre1N  40375  cdlemefs29clN  40376  cdleme43fsv1snlem  40377  cdlemefs32fvaN  40379  cdlemefs32fva1  40380  cdlemefs31fv1  40381  cdleme36a  40417  cdleme39a  40422  cdleme42a  40428  cdleme42c  40429  cdleme17d3  40453  cdleme48fv  40456  cdleme48bw  40459  cdleme48b  40460  cdlemeg46rgv  40485  cdlemeg46req  40486  cdlemeg46gfv  40487  cdleme48d  40492  cdleme50trn2a  40507  cdleme50trn2  40508  cdleme50ltrn  40514  cdlemf1  40518  cdlemf  40520  trlord  40526  cdlemg2dN  40547  cdlemg2fvlem  40551  cdlemg2l  40560  cdlemg7fvbwN  40564  cdlemg7aN  40582  cdlemg10bALTN  40593  cdlemg10c  40596  cdlemg17a  40618  cdlemg17dALTN  40621  cdlemg31b0a  40652  cdlemg31a  40654  cdlemg31b  40655  cdlemg34  40669  cdlemg36  40671  ltrnco  40676  trlcoabs2N  40679  trlcolem  40683  cdlemg48  40694  tgrpov  40705  tendoco2  40725  tendoplco2  40736  cdlemh1  40772  cdlemi1  40775  cdlemi2  40776  cdlemj3  40780  tendoid0  40782  cdlemk1  40788  cdlemk2  40789  cdlemk4  40791  cdlemk8  40795  cdlemk9  40796  cdlemk9bN  40797  cdlemk10  40800  cdlemk26b-3  40862  cdlemk26-3  40863  cdlemk28-3  40865  cdlemk37  40871  cdlemk39  40873  cdlemkfid1N  40878  cdlemkid1  40879  cdlemky  40883  cdlemkyu  40884  cdlemk19ylem  40887  cdlemk19xlem  40899  cdlemk11t  40903  cdlemk51  40910  cdlemkyyN  40919  cdleml6  40938  cdleml7  40939  cdleml8  40940  cdleml9  40941  erngdvlem4  40948  erngdvlem4-rN  40956  tendospcanN  40980  dia11N  41005  cdlemm10N  41075  dib11N  41117  dicvaddcl  41147  dicvscacl  41148  cdlemn6  41159  dihvalcq2  41204  dihopelvalcpre  41205  dihord6b  41217  dihord5apre  41219  dihmeetlem1N  41247  dihmeetlem2N  41256  dihglbcpreN  41257  dihjatc1  41268  dihmeetlem20N  41283  dih1dimatlem0  41285  dihatlat  41291  dihglblem6  41297  dochexmidlem4  41420  mapdpglem32  41662  mapdh8ad  41736  mapdh9aOLDN  41747  hdmap11lem2  41799  hdmap14lem6  41830  frlmfzowrdb  42459  flt4lem5  42605  mzpsubst  42704  pellex  42791  pellfundex  42842  pellfund14gap  42843  qirropth  42864  rmxypos  42904  congmul  42924  congsub  42927  mzpcong  42929  coprmdvdsb  42942  jm2.15nn0  42960  jm2.16nn0  42961  rpnnen3lem  42988  idomsubgmo  43154  relexp01min  43675  mullimc  45537  islptre  45540  limccog  45541  mullimcf  45544  addlimc  45569  0ellimcdiv  45570  limsupre3lem  45653  stoweidlem57  45978  fourierdlem48  46075  fourierdlem80  46107  fourierdlem113  46140  ovncvrrp  46485  opnvonmbllem2  46554  ovolval5lem3  46575  ovnovollem3  46579  itsclc0lem1  48490  itsclc0lem2  48491  itschlc0yqe  48494  itscnhlc0xyqsol  48499  itschlc0xyqsol1  48500