Theorem simp3l 1220

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp13l  1307  simp23l  1313  simp33l  1319  tfisi  7864  fpr3g  8291  tfrlem5  8375  omeulem1  8576  omeulem2  8577  uniinqs  8804  elfiun  9400  tcrank  9866  isfin2-2  10321  konigthlem  10571  gruen  10815  addlid  11411  mulcan  11869  mulcan2  11870  divass  11908  divdir  11915  muldivdir  11925  subdivcomb1  11928  subdivcomb2  11929  divcan5  11935  ltmul1  12083  ltdiv1  12097  ltmuldiv  12106  lediv2  12123  xaddass2  13294  xlt2add  13304  xmulasslem3  13330  xadddi2  13341  expaddz  14162  expmulz  14164  muldivbinom2  14319  resqrtcl  15330  o1add  15691  o1mul  15692  o1sub  15693  dvdsadd2b  16389  dvdsgcd  16627  rpexp12i  16808  pythagtriplem3  16903  pcpremul  16928  pceu  16931  pcqmul  16938  pcqdiv  16942  setsstruct  17261  f1ocpbllem  17603  funcoppc  17957  funcres  17978  catcisolem  18192  1stfcl  18278  2ndfcl  18279  prfcl  18284  evlfcl  18303  curf1cl  18309  curfcl  18313  hofcl  18340  latjlej12  18536  latmlem12  18552  latj4  18570  latj4rot  18571  symgsssg  19568  symgfisg  19569  psgnunilem4  19598  odcong  19650  cmn4  19902  ablsub4  19911  abladdsub4  19912  lsm4  19961  abvdom  20970  abvres  20971  abvtrivd  20972  orngmul  21005  lspsolvlem  21303  lbsextlem2  21320  lidlsubcl  21386  frlmbas3  21963  matmulcell  22639  marrepeval  22757  ma1repveval  22765  submaeval  22776  mdetunilem3  22808  mdetuni0  22815  mdetmul  22817  minmar1eval  22843  nllyrest  23680  hausflimlem  24173  tsmsxp  24349  psmetlecl  24509  xmetlecl  24540  prdsxmetlem  24562  ngpocelbl  24898  bndth  25154  cph2ass  25409  iscau3  25474  dvres2  26108  coemullem  26444  vieta1  26510  aalioulem4  26535  cxpcn3lem  26949  angcan  27004  dchrvmasumlema  27701  logdivsum  27734  abvcxp  27816  padicabv  27831  nosupbnd1lem4  27912  nosupbnd1lem5  27913  noinfbnd1lem4  27927  cofcut1  28150  cofcut2  28152  divmulsw  28423  precsexlem8  28444  precsexlem9  28445  bdayfinbndlem1  28697  ax5seglem3  29318  ax5seglem6  29321  axpasch  29328  axeuclid  29350  axcontlem4  29354  axcontlem8  29358  wlkl1loop  30024  trlsonwlkon  30094  pthontrlon  30133  wspthsswwlknon  30307  frgr2wwlkeqm  30719  adjlnop  32475  xreceu  33278  rhmdvd  33675  measvunilem  34634  measvunilem0  34635  measres  34644  bnj1128  35410  umgr2cycllem  35653  umgr2cycl  35654  satfv1fvfmla1  35936  cgrcomim  36502  cgrcoml  36509  cgrcomr  36510  cgrdegen  36517  segconeu  36524  btwnintr  36532  btwnexch3  36533  btwnouttr2  36535  btwnouttr  36537  btwnexch  36538  trisegint  36541  lineext  36589  linecgr  36594  lineid  36596  idinside  36597  btwnconn1lem3  36602  btwnconn1lem4  36603  btwnconn1lem7  36606  btwnconn1lem14  36613  btwnconn2  36615  midofsegid  36617  btwnoutside  36638  outsideoftr  36642  lineunray  36660  lineelsb2  36661  cnres2  38455  heibor  38513  lsmcv2  39844  lcvat  39845  lcvexchlem4  39852  lcvexchlem5  39853  lfladd  39881  lflsub  39882  lflmul  39883  lshpkrlem4  39928  latm4  40048  omlmod1i2N  40075  cvlatexch3  40153  cvlsupr7  40163  hlatj4  40189  hlrelat3  40227  cvrval3  40228  atcvrj1  40246  atlelt  40253  2atlt  40254  2atjm  40260  3noncolr2  40264  athgt  40271  3dimlem2  40274  3dimlem4  40279  3dimlem4OLDN  40280  3dim3  40284  1cvratex  40288  ps-1  40292  ps-2  40293  hlatexch3N  40295  llnle  40333  atcvrlln2  40334  atcvrlln  40335  lplni2  40352  lplnle  40355  lplnnle2at  40356  llncvrlpln2  40372  lplnexllnN  40379  2llnmeqat  40386  lvolnle3at  40397  4atlem0ae  40409  lplncvrlvol2  40430  lnjatN  40595  lncvrat  40597  cdlemblem  40608  elpaddri  40617  paddasslem2  40636  paddasslem16  40650  padd4N  40655  hlmod1i  40671  dalawlem2  40687  pclfinN  40715  pexmidlem4N  40788  pl42lem1N  40794  lhp2lt  40816  lhpexle1  40823  lhpexle2lem  40824  lhpj1  40837  lhpmcvr5N  40842  lhp2at0  40847  lhp2atnle  40848  lhp2at0nle  40850  lhple  40857  lhpat  40858  lhpat4N  40859  4atexlempnq  40870  4atexlem7  40890  4atex  40891  ltrn11  40941  ltrnle  40944  ltrnm  40946  ltrnj  40947  ltrncvr  40948  ltrnel  40954  ltrncnvel  40957  ltrncnv  40961  trlval2  40978  trlcnv  40980  trljat1  40981  trljat2  40982  trlat  40984  trl0  40985  trlnidat  40988  trlnid  40994  cdlemc1  41006  cdlemc2  41007  cdlemc5  41010  cdlemd2  41014  cdlemd7  41019  cdlemd8  41020  cdlemd9  41021  cdleme0e  41032  cdleme3g  41049  cdleme3h  41050  cdleme3  41052  cdleme5  41055  cdleme10  41069  cdleme11a  41075  cdleme11c  41076  cdleme11h  41081  cdleme11j  41082  cdleme0nex  41105  cdleme18a  41106  cdleme18b  41107  cdleme22gb  41109  cdleme20zN  41116  cdleme20c  41126  cdleme20k  41134  cdleme21a  41140  cdleme21b  41141  cdleme21c  41142  cdleme21h  41149  cdleme22b  41156  cdleme22d  41158  cdleme22f  41161  cdleme25a  41168  cdleme25c  41170  cdleme25dN  41171  cdleme26ee  41175  cdleme30a  41193  cdlemefr29bpre0N  41221  cdlemefr29clN  41222  cdlemefr32fvaN  41224  cdlemefr32fva1  41225  cdlemefs29bpre0N  41231  cdlemefs29bpre1N  41232  cdlemefs29cpre1N  41233  cdlemefs29clN  41234  cdleme43fsv1snlem  41235  cdlemefs32fvaN  41237  cdlemefs32fva1  41238  cdlemefs31fv1  41239  cdleme36a  41275  cdleme39a  41280  cdleme42a  41286  cdleme42c  41287  cdleme17d3  41311  cdleme48fv  41314  cdleme48bw  41317  cdleme48b  41318  cdlemeg46rgv  41343  cdlemeg46req  41344  cdlemeg46gfv  41345  cdleme48d  41350  cdleme50trn2a  41365  cdleme50trn2  41366  cdleme50ltrn  41372  cdlemf1  41376  cdlemf  41378  trlord  41384  cdlemg2dN  41405  cdlemg2fvlem  41409  cdlemg2l  41418  cdlemg7fvbwN  41422  cdlemg7aN  41440  cdlemg10bALTN  41451  cdlemg10c  41454  cdlemg17a  41476  cdlemg17dALTN  41479  cdlemg31b0a  41510  cdlemg31a  41512  cdlemg31b  41513  cdlemg34  41527  cdlemg36  41529  ltrnco  41534  trlcoabs2N  41537  trlcolem  41541  cdlemg48  41552  tgrpov  41563  tendoco2  41583  tendoplco2  41594  cdlemh1  41630  cdlemi1  41633  cdlemi2  41634  cdlemj3  41638  tendoid0  41640  cdlemk1  41646  cdlemk2  41647  cdlemk4  41649  cdlemk8  41653  cdlemk9  41654  cdlemk9bN  41655  cdlemk10  41658  cdlemk26b-3  41720  cdlemk26-3  41721  cdlemk28-3  41723  cdlemk37  41729  cdlemk39  41731  cdlemkfid1N  41736  cdlemkid1  41737  cdlemky  41741  cdlemkyu  41742  cdlemk19ylem  41745  cdlemk19xlem  41757  cdlemk11t  41761  cdlemk51  41768  cdlemkyyN  41777  cdleml6  41796  cdleml7  41797  cdleml8  41798  cdleml9  41799  erngdvlem4  41806  erngdvlem4-rN  41814  tendospcanN  41838  dia11N  41863  cdlemm10N  41933  dib11N  41975  dicvaddcl  42005  dicvscacl  42006  cdlemn6  42017  dihvalcq2  42062  dihopelvalcpre  42063  dihord6b  42075  dihord5apre  42077  dihmeetlem1N  42105  dihmeetlem2N  42114  dihglbcpreN  42115  dihjatc1  42126  dihmeetlem20N  42141  dih1dimatlem0  42143  dihatlat  42149  dihglblem6  42155  dochexmidlem4  42278  mapdpglem32  42520  mapdh8ad  42594  mapdh9aOLDN  42605  hdmap11lem2  42657  hdmap14lem6  42688  frlmfzowrdb  43319  flt4lem5  43423  mzpsubst  43520  pellex  43603  pellfundex  43654  pellfund14gap  43655  qirropth  43676  rmxypos  43715  congmul  43735  congsub  43738  mzpcong  43740  coprmdvdsb  43753  jm2.15nn0  43771  jm2.16nn0  43772  rpnnen3lem  43799  idomsubgmo  43961  relexp01min  44480  mullimc  46373  islptre  46376  limccog  46377  mullimcf  46380  addlimc  46403  0ellimcdiv  46404  limsupre3lem  46487  stoweidlem57  46812  fourierdlem48  46909  fourierdlem80  46941  fourierdlem113  46974  ovncvrrp  47319  opnvonmbllem2  47388  ovolval5lem3  47409  ovnovollem3  47413  grlimedgclnbgr  48801  itsclc0lem1  49577  itsclc0lem2  49578  itschlc0yqe  49581  itscnhlc0xyqsol  49586  itschlc0xyqsol1  49587  swapffunc  50101  fucofunc  50178  fucoppc  50229