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  7870  fpr3g  8306  tfrlem5  8390  omeulem1  8593  omeulem2  8594  uniinqs  8821  elfiun  9425  tcrank  9904  isfin2-2  10400  konigthlem  10656  gruen  10900  addlid  11496  mulcan  11956  mulcan2  11957  divass  11995  divdir  12002  muldivdir  12012  subdivcomb1  12015  subdivcomb2  12016  divcan5  12022  ltmul1  12170  ltdiv1  12184  ltmuldiv  12193  lediv2  12210  xaddass2  13383  xlt2add  13393  xmulasslem3  13419  xadddi2  13430  expaddz  14252  expmulz  14254  muldivbinom2  14410  resqrtcl  15425  o1add  15786  o1mul  15787  o1sub  15788  dvdsadd2b  16481  dvdsgcd  16722  rpexp12i  16905  pythagtriplem3  17001  pcpremul  17026  pceu  17029  pcqmul  17036  pcqdiv  17040  setsstruct  17359  f1ocpbllem  17701  funcoppc  18055  funcres  18076  catcisolem  18290  1stfcl  18376  2ndfcl  18377  prfcl  18382  evlfcl  18401  curf1cl  18407  curfcl  18411  hofcl  18438  latjlej12  18634  latmlem12  18650  latj4  18668  latj4rot  18669  symgsssg  19686  symgfisg  19687  psgnunilem4  19716  odcong  19768  cmn4  20020  ablsub4  20029  abladdsub4  20030  lsm4  20079  abvdom  21092  abvres  21093  abvtrivd  21094  orngmul  21127  lspsolvlem  21425  lbsextlem2  21442  lidlsubcl  21508  frlmbas3  22087  matmulcell  22765  marrepeval  22883  ma1repveval  22891  submaeval  22902  mdetunilem3  22934  mdetuni0  22941  mdetmul  22943  minmar1eval  22969  nllyrest  23810  hausflimlem  24303  tsmsxp  24479  psmetlecl  24639  xmetlecl  24670  prdsxmetlem  24692  ngpocelbl  25028  bndth  25284  cph2ass  25539  iscau3  25604  dvres2  26237  coemullem  26574  vieta1  26640  aalioulem4  26667  cxpcn3lem  27080  angcan  27135  dchrvmasumlema  27832  logdivsum  27865  abvcxp  27947  padicabv  27962  flt4lem5  27985  nosupbnd1lem4  28073  nosupbnd1lem5  28074  noinfbnd1lem4  28088  cofcut1  28311  cofcut2  28313  divmulsw  28584  precsexlem8  28605  precsexlem9  28606  bdayfinbndlem1  28858  ax5seglem3  29514  ax5seglem6  29517  axpasch  29524  axeuclid  29546  axcontlem4  29550  axcontlem8  29554  wlkl1loop  30223  trlsonwlkon  30297  pthontrlon  30338  wspthsswwlknon  30515  umgr2cycllem  30751  umgr2cycl  30752  frgr2wwlkeqm  30937  adjlnop  32693  xreceu  33534  rhmdvd  33931  measvunilem  34891  measvunilem0  34892  measres  34901  bnj1128  35666  satfv1fvfmla1  36274  cgrcomim  36846  cgrcoml  36853  cgrcomr  36854  cgrdegen  36861  segconeu  36868  btwnintr  36876  btwnexch3  36877  btwnouttr2  36879  btwnouttr  36881  btwnexch  36882  trisegint  36885  lineext  36933  linecgr  36938  lineid  36940  idinside  36941  btwnconn1lem3  36946  btwnconn1lem4  36947  btwnconn1lem7  36950  btwnconn1lem14  36957  btwnconn2  36959  midofsegid  36961  btwnoutside  36982  outsideoftr  36986  lineunray  37004  lineelsb2  37005  cnres2  38790  heibor  38848  lsmcv2  40179  lcvat  40180  lcvexchlem4  40187  lcvexchlem5  40188  lfladd  40216  lflsub  40217  lflmul  40218  lshpkrlem4  40263  latm4  40383  omlmod1i2N  40410  cvlatexch3  40488  cvlsupr7  40498  hlatj4  40524  hlrelat3  40562  cvrval3  40563  atcvrj1  40581  atlelt  40588  2atlt  40589  2atjm  40595  3noncolr2  40599  athgt  40606  3dimlem2  40609  3dimlem4  40614  3dimlem4OLDN  40615  3dim3  40619  1cvratex  40623  ps-1  40627  ps-2  40628  hlatexch3N  40630  llnle  40668  atcvrlln2  40669  atcvrlln  40670  lplni2  40687  lplnle  40690  lplnnle2at  40691  llncvrlpln2  40707  lplnexllnN  40714  2llnmeqat  40721  lvolnle3at  40732  4atlem0ae  40744  lplncvrlvol2  40765  lnjatN  40930  lncvrat  40932  cdlemblem  40943  elpaddri  40952  paddasslem2  40971  paddasslem16  40985  padd4N  40990  hlmod1i  41006  dalawlem2  41022  pclfinN  41050  pexmidlem4N  41123  pl42lem1N  41129  lhp2lt  41151  lhpexle1  41158  lhpexle2lem  41159  lhpj1  41172  lhpmcvr5N  41177  lhp2at0  41182  lhp2atnle  41183  lhp2at0nle  41185  lhple  41192  lhpat  41193  lhpat4N  41194  4atexlempnq  41205  4atexlem7  41225  4atex  41226  ltrn11  41276  ltrnle  41279  ltrnm  41281  ltrnj  41282  ltrncvr  41283  ltrnel  41289  ltrncnvel  41292  ltrncnv  41296  trlval2  41313  trlcnv  41315  trljat1  41316  trljat2  41317  trlat  41319  trl0  41320  trlnidat  41323  trlnid  41329  cdlemc1  41341  cdlemc2  41342  cdlemc5  41345  cdlemd2  41349  cdlemd7  41354  cdlemd8  41355  cdlemd9  41356  cdleme0e  41367  cdleme3g  41384  cdleme3h  41385  cdleme3  41387  cdleme5  41390  cdleme10  41404  cdleme11a  41410  cdleme11c  41411  cdleme11h  41416  cdleme11j  41417  cdleme0nex  41440  cdleme18a  41441  cdleme18b  41442  cdleme22gb  41444  cdleme20zN  41451  cdleme20c  41461  cdleme20k  41469  cdleme21a  41475  cdleme21b  41476  cdleme21c  41477  cdleme21h  41484  cdleme22b  41491  cdleme22d  41493  cdleme22f  41496  cdleme25a  41503  cdleme25c  41505  cdleme25dN  41506  cdleme26ee  41510  cdleme30a  41528  cdlemefr29bpre0N  41556  cdlemefr29clN  41557  cdlemefr32fvaN  41559  cdlemefr32fva1  41560  cdlemefs29bpre0N  41566  cdlemefs29bpre1N  41567  cdlemefs29cpre1N  41568  cdlemefs29clN  41569  cdleme43fsv1snlem  41570  cdlemefs32fvaN  41572  cdlemefs32fva1  41573  cdlemefs31fv1  41574  cdleme36a  41610  cdleme39a  41615  cdleme42a  41621  cdleme42c  41622  cdleme17d3  41646  cdleme48fv  41649  cdleme48bw  41652  cdleme48b  41653  cdlemeg46rgv  41678  cdlemeg46req  41679  cdlemeg46gfv  41680  cdleme48d  41685  cdleme50trn2a  41700  cdleme50trn2  41701  cdleme50ltrn  41707  cdlemf1  41711  cdlemf  41713  trlord  41719  cdlemg2dN  41740  cdlemg2fvlem  41744  cdlemg2l  41753  cdlemg7fvbwN  41757  cdlemg7aN  41775  cdlemg10bALTN  41786  cdlemg10c  41789  cdlemg17a  41811  cdlemg17dALTN  41814  cdlemg31b0a  41845  cdlemg31a  41847  cdlemg31b  41848  cdlemg34  41862  cdlemg36  41864  ltrnco  41869  trlcoabs2N  41872  trlcolem  41876  cdlemg48  41887  tgrpov  41898  tendoco2  41918  tendoplco2  41929  cdlemh1  41965  cdlemi1  41968  cdlemi2  41969  cdlemj3  41973  tendoid0  41975  cdlemk1  41981  cdlemk2  41982  cdlemk4  41984  cdlemk8  41988  cdlemk9  41989  cdlemk9bN  41990  cdlemk10  41993  cdlemk26b-3  42055  cdlemk26-3  42056  cdlemk28-3  42058  cdlemk37  42064  cdlemk39  42066  cdlemkfid1N  42071  cdlemkid1  42072  cdlemky  42076  cdlemkyu  42077  cdlemk19ylem  42080  cdlemk19xlem  42092  cdlemk11t  42096  cdlemk51  42103  cdlemkyyN  42112  cdleml6  42131  cdleml7  42132  cdleml8  42133  cdleml9  42134  erngdvlem4  42141  erngdvlem4-rN  42149  tendospcanN  42173  dia11N  42198  cdlemm10N  42268  dib11N  42310  dicvaddcl  42340  dicvscacl  42341  cdlemn6  42352  dihvalcq2  42397  dihopelvalcpre  42398  dihord6b  42410  dihord5apre  42412  dihmeetlem1N  42440  dihmeetlem2N  42449  dihglbcpreN  42450  dihjatc1  42461  dihmeetlem20N  42476  dih1dimatlem0  42478  dihatlat  42484  dihglblem6  42490  dochexmidlem4  42613  mapdpglem32  42855  mapdh8ad  42929  mapdh9aOLDN  42940  hdmap11lem2  42992  hdmap14lem6  43023  frlmfzowrdb  43664  mzpsubst  43852  pellex  43935  pellfundex  43986  pellfund14gap  43987  qirropth  44008  rmxypos  44047  congmul  44067  congsub  44070  mzpcong  44072  coprmdvdsb  44085  jm2.15nn0  44103  jm2.16nn0  44104  rpnnen3lem  44131  idomsubgmo  44288  relexp01min  44806  mullimc  46721  islptre  46724  limccog  46725  mullimcf  46728  addlimc  46751  0ellimcdiv  46752  limsupre3lem  46835  stoweidlem57  47160  fourierdlem48  47257  fourierdlem80  47289  fourierdlem113  47322  ovncvrrp  47667  opnvonmbllem2  47736  ovolval5lem3  47757  ovnovollem3  47761  grlimedgclnbgr  49186  itsclc0lem1  49961  itsclc0lem2  49962  itschlc0yqe  49965  itscnhlc0xyqsol  49970  itschlc0xyqsol1  49971  swapffunc  50497  fucofunc  50574  fucoppc  50638  parmapfunc2  50867  parmapfunc  50868