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  7799  fpr3g  8225  tfrlem5  8309  omeulem1  8507  omeulem2  8508  uniinqs  8731  elfiun  9339  tcrank  9799  isfin2-2  10232  konigthlem  10481  gruen  10725  addlid  11317  mulcan  11775  mulcan2  11776  divass  11815  divdir  11822  div11OLD  11826  muldivdir  11835  subdivcomb1  11837  subdivcomb2  11838  divcan5  11844  ltmul1  11992  ltdiv1  12007  ltmuldiv  12016  lediv2  12033  xaddass2  13170  xlt2add  13180  xmulasslem3  13206  xadddi2  13217  expaddz  14031  expmulz  14033  muldivbinom2  14188  resqrtcl  15178  o1add  15539  o1mul  15540  o1sub  15541  dvdsadd2b  16235  dvdsgcd  16473  rpexp12i  16653  pythagtriplem3  16748  pcpremul  16773  pceu  16776  pcqmul  16783  pcqdiv  16787  setsstruct  17105  f1ocpbllem  17446  funcoppc  17800  funcres  17821  catcisolem  18035  1stfcl  18121  2ndfcl  18122  prfcl  18127  evlfcl  18146  curf1cl  18152  curfcl  18156  hofcl  18183  latjlej12  18379  latmlem12  18395  latj4  18413  latj4rot  18414  symgsssg  19364  symgfisg  19365  psgnunilem4  19394  odcong  19446  cmn4  19698  ablsub4  19707  abladdsub4  19708  lsm4  19757  abvdom  20733  abvres  20734  abvtrivd  20735  orngmul  20768  lspsolvlem  21067  lbsextlem2  21084  lidlsubcl  21149  frlmbas3  21701  matmulcell  22348  marrepeval  22466  ma1repveval  22474  submaeval  22485  mdetunilem3  22517  mdetuni0  22524  mdetmul  22526  minmar1eval  22552  nllyrest  23389  hausflimlem  23882  tsmsxp  24058  psmetlecl  24219  xmetlecl  24250  prdsxmetlem  24272  ngpocelbl  24608  bndth  24873  cph2ass  25129  iscau3  25194  dvres2  25829  coemullem  26171  vieta1  26236  aalioulem4  26259  cxpcn3lem  26673  angcan  26728  dchrvmasumlema  27427  logdivsum  27460  abvcxp  27542  padicabv  27557  nosupbnd1lem4  27639  nosupbnd1lem5  27640  noinfbnd1lem4  27654  cofcut1  27851  cofcut2  27853  divsmulw  28119  precsexlem8  28139  precsexlem9  28140  ax5seglem3  28894  ax5seglem6  28897  axpasch  28904  axeuclid  28926  axcontlem4  28930  axcontlem8  28934  wlkl1loop  29601  trlsonwlkon  29671  pthontrlon  29710  wspthsswwlknon  29884  frgr2wwlkeqm  30293  adjlnop  32048  xreceu  32875  rhmdvd  33272  measvunilem  34178  measvunilem0  34179  measres  34188  bnj1128  34956  umgr2cycllem  35112  umgr2cycl  35113  satfv1fvfmla1  35395  cgrcomim  35962  cgrcoml  35969  cgrcomr  35970  cgrdegen  35977  segconeu  35984  btwnintr  35992  btwnexch3  35993  btwnouttr2  35995  btwnouttr  35997  btwnexch  35998  trisegint  36001  lineext  36049  linecgr  36054  lineid  36056  idinside  36057  btwnconn1lem3  36062  btwnconn1lem4  36063  btwnconn1lem7  36066  btwnconn1lem14  36073  btwnconn2  36075  midofsegid  36077  btwnoutside  36098  outsideoftr  36102  lineunray  36120  lineelsb2  36121  cnres2  37742  heibor  37800  lsmcv2  39007  lcvat  39008  lcvexchlem4  39015  lcvexchlem5  39016  lfladd  39044  lflsub  39045  lflmul  39046  lshpkrlem4  39091  latm4  39211  omlmod1i2N  39238  cvlatexch3  39316  cvlsupr7  39326  hlatj4  39352  hlrelat3  39391  cvrval3  39392  atcvrj1  39410  atlelt  39417  2atlt  39418  2atjm  39424  3noncolr2  39428  athgt  39435  3dimlem2  39438  3dimlem4  39443  3dimlem4OLDN  39444  3dim3  39448  1cvratex  39452  ps-1  39456  ps-2  39457  hlatexch3N  39459  llnle  39497  atcvrlln2  39498  atcvrlln  39499  lplni2  39516  lplnle  39519  lplnnle2at  39520  llncvrlpln2  39536  lplnexllnN  39543  2llnmeqat  39550  lvolnle3at  39561  4atlem0ae  39573  lplncvrlvol2  39594  lnjatN  39759  lncvrat  39761  cdlemblem  39772  elpaddri  39781  paddasslem2  39800  paddasslem16  39814  padd4N  39819  hlmod1i  39835  dalawlem2  39851  pclfinN  39879  pexmidlem4N  39952  pl42lem1N  39958  lhp2lt  39980  lhpexle1  39987  lhpexle2lem  39988  lhpj1  40001  lhpmcvr5N  40006  lhp2at0  40011  lhp2atnle  40012  lhp2at0nle  40014  lhple  40021  lhpat  40022  lhpat4N  40023  4atexlempnq  40034  4atexlem7  40054  4atex  40055  ltrn11  40105  ltrnle  40108  ltrnm  40110  ltrnj  40111  ltrncvr  40112  ltrnel  40118  ltrncnvel  40121  ltrncnv  40125  trlval2  40142  trlcnv  40144  trljat1  40145  trljat2  40146  trlat  40148  trl0  40149  trlnidat  40152  trlnid  40158  cdlemc1  40170  cdlemc2  40171  cdlemc5  40174  cdlemd2  40178  cdlemd7  40183  cdlemd8  40184  cdlemd9  40185  cdleme0e  40196  cdleme3g  40213  cdleme3h  40214  cdleme3  40216  cdleme5  40219  cdleme10  40233  cdleme11a  40239  cdleme11c  40240  cdleme11h  40245  cdleme11j  40246  cdleme0nex  40269  cdleme18a  40270  cdleme18b  40271  cdleme22gb  40273  cdleme20zN  40280  cdleme20c  40290  cdleme20k  40298  cdleme21a  40304  cdleme21b  40305  cdleme21c  40306  cdleme21h  40313  cdleme22b  40320  cdleme22d  40322  cdleme22f  40325  cdleme25a  40332  cdleme25c  40334  cdleme25dN  40335  cdleme26ee  40339  cdleme30a  40357  cdlemefr29bpre0N  40385  cdlemefr29clN  40386  cdlemefr32fvaN  40388  cdlemefr32fva1  40389  cdlemefs29bpre0N  40395  cdlemefs29bpre1N  40396  cdlemefs29cpre1N  40397  cdlemefs29clN  40398  cdleme43fsv1snlem  40399  cdlemefs32fvaN  40401  cdlemefs32fva1  40402  cdlemefs31fv1  40403  cdleme36a  40439  cdleme39a  40444  cdleme42a  40450  cdleme42c  40451  cdleme17d3  40475  cdleme48fv  40478  cdleme48bw  40481  cdleme48b  40482  cdlemeg46rgv  40507  cdlemeg46req  40508  cdlemeg46gfv  40509  cdleme48d  40514  cdleme50trn2a  40529  cdleme50trn2  40530  cdleme50ltrn  40536  cdlemf1  40540  cdlemf  40542  trlord  40548  cdlemg2dN  40569  cdlemg2fvlem  40573  cdlemg2l  40582  cdlemg7fvbwN  40586  cdlemg7aN  40604  cdlemg10bALTN  40615  cdlemg10c  40618  cdlemg17a  40640  cdlemg17dALTN  40643  cdlemg31b0a  40674  cdlemg31a  40676  cdlemg31b  40677  cdlemg34  40691  cdlemg36  40693  ltrnco  40698  trlcoabs2N  40701  trlcolem  40705  cdlemg48  40716  tgrpov  40727  tendoco2  40747  tendoplco2  40758  cdlemh1  40794  cdlemi1  40797  cdlemi2  40798  cdlemj3  40802  tendoid0  40804  cdlemk1  40810  cdlemk2  40811  cdlemk4  40813  cdlemk8  40817  cdlemk9  40818  cdlemk9bN  40819  cdlemk10  40822  cdlemk26b-3  40884  cdlemk26-3  40885  cdlemk28-3  40887  cdlemk37  40893  cdlemk39  40895  cdlemkfid1N  40900  cdlemkid1  40901  cdlemky  40905  cdlemkyu  40906  cdlemk19ylem  40909  cdlemk19xlem  40921  cdlemk11t  40925  cdlemk51  40932  cdlemkyyN  40941  cdleml6  40960  cdleml7  40961  cdleml8  40962  cdleml9  40963  erngdvlem4  40970  erngdvlem4-rN  40978  tendospcanN  41002  dia11N  41027  cdlemm10N  41097  dib11N  41139  dicvaddcl  41169  dicvscacl  41170  cdlemn6  41181  dihvalcq2  41226  dihopelvalcpre  41227  dihord6b  41239  dihord5apre  41241  dihmeetlem1N  41269  dihmeetlem2N  41278  dihglbcpreN  41279  dihjatc1  41290  dihmeetlem20N  41305  dih1dimatlem0  41307  dihatlat  41313  dihglblem6  41319  dochexmidlem4  41442  mapdpglem32  41684  mapdh8ad  41758  mapdh9aOLDN  41769  hdmap11lem2  41821  hdmap14lem6  41852  frlmfzowrdb  42477  flt4lem5  42623  mzpsubst  42721  pellex  42808  pellfundex  42859  pellfund14gap  42860  qirropth  42881  rmxypos  42920  congmul  42940  congsub  42943  mzpcong  42945  coprmdvdsb  42958  jm2.15nn0  42976  jm2.16nn0  42977  rpnnen3lem  43004  idomsubgmo  43166  relexp01min  43686  mullimc  45598  islptre  45601  limccog  45602  mullimcf  45605  addlimc  45630  0ellimcdiv  45631  limsupre3lem  45714  stoweidlem57  46039  fourierdlem48  46136  fourierdlem80  46168  fourierdlem113  46201  ovncvrrp  46546  opnvonmbllem2  46615  ovolval5lem3  46636  ovnovollem3  46640  grlimedgclnbgr  47980  itsclc0lem1  48742  itsclc0lem2  48743  itschlc0yqe  48746  itscnhlc0xyqsol  48751  itschlc0xyqsol1  48752  swapffunc  49268  fucofunc  49345  fucoppc  49396