Theorem simp3l 1199

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 1133	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp13l  1286  simp23l  1292  simp33l  1298  tfisi  7863  fpr3g  8291  tfrlem5  8401  omeulem1  8603  omeulem2  8604  uniinqs  8816  elfiun  9454  tcrank  9908  isfin2-2  10343  konigthlem  10592  gruen  10836  addlid  11428  mulcan  11882  mulcan2  11883  divass  11921  divdir  11928  div11  11931  muldivdir  11938  subdivcomb1  11940  subdivcomb2  11941  divcan5  11947  ltmul1  12095  ltdiv1  12109  ltmuldiv  12118  lediv2  12135  xaddass2  13262  xlt2add  13272  xmulasslem3  13298  xadddi2  13309  expaddz  14104  expmulz  14106  muldivbinom2  14255  resqrtcl  15233  o1add  15591  o1mul  15592  o1sub  15593  dvdsadd2b  16283  dvdsgcd  16520  rpexp12i  16696  pythagtriplem3  16787  pcpremul  16812  pceu  16815  pcqmul  16822  pcqdiv  16826  setsstruct  17145  f1ocpbllem  17506  funcoppc  17861  funcres  17882  catcisolem  18099  1stfcl  18188  2ndfcl  18189  prfcl  18194  evlfcl  18214  curf1cl  18220  curfcl  18224  hofcl  18251  latjlej12  18447  latmlem12  18463  latj4  18481  latj4rot  18482  symgsssg  19422  symgfisg  19423  psgnunilem4  19452  odcong  19504  cmn4  19756  ablsub4  19765  abladdsub4  19766  lsm4  19815  abvdom  20718  abvres  20719  abvtrivd  20720  lspsolvlem  21030  lbsextlem2  21047  lidlsubcl  21120  frlmbas3  21710  matmulcell  22360  marrepeval  22478  ma1repveval  22486  submaeval  22497  mdetunilem3  22529  mdetuni0  22536  mdetmul  22538  minmar1eval  22564  nllyrest  23403  hausflimlem  23896  tsmsxp  24072  psmetlecl  24234  xmetlecl  24265  prdsxmetlem  24287  ngpocelbl  24634  bndth  24897  cph2ass  25154  iscau3  25219  dvres2  25854  coemullem  26197  vieta1  26260  aalioulem4  26283  cxpcn3lem  26695  angcan  26747  dchrvmasumlema  27446  logdivsum  27479  abvcxp  27561  padicabv  27576  nosupbnd1lem4  27657  nosupbnd1lem5  27658  noinfbnd1lem4  27672  cofcut1  27853  cofcut2  27855  divsmulw  28105  precsexlem8  28125  precsexlem9  28126  ax5seglem3  28755  ax5seglem6  28758  axpasch  28765  axeuclid  28787  axcontlem4  28791  axcontlem8  28795  wlkl1loop  29465  trlsonwlkon  29537  pthontrlon  29574  wspthsswwlknon  29745  frgr2wwlkeqm  30154  adjlnop  31909  xreceu  32658  orngmul  33031  rhmdvd  33046  measvunilem  33831  measvunilem0  33832  measres  33841  bnj1128  34621  umgr2cycllem  34750  umgr2cycl  34751  satfv1fvfmla1  35033  cgrcomim  35585  cgrcoml  35592  cgrcomr  35593  cgrdegen  35600  segconeu  35607  btwnintr  35615  btwnexch3  35616  btwnouttr2  35618  btwnouttr  35620  btwnexch  35621  trisegint  35624  lineext  35672  linecgr  35677  lineid  35679  idinside  35680  btwnconn1lem3  35685  btwnconn1lem4  35686  btwnconn1lem7  35689  btwnconn1lem14  35696  btwnconn2  35698  midofsegid  35700  btwnoutside  35721  outsideoftr  35725  lineunray  35743  lineelsb2  35744  cnres2  37236  heibor  37294  lsmcv2  38501  lcvat  38502  lcvexchlem4  38509  lcvexchlem5  38510  lfladd  38538  lflsub  38539  lflmul  38540  lshpkrlem4  38585  latm4  38705  omlmod1i2N  38732  cvlatexch3  38810  cvlsupr7  38820  hlatj4  38846  hlrelat3  38885  cvrval3  38886  atcvrj1  38904  atlelt  38911  2atlt  38912  2atjm  38918  3noncolr2  38922  athgt  38929  3dimlem2  38932  3dimlem4  38937  3dimlem4OLDN  38938  3dim3  38942  1cvratex  38946  ps-1  38950  ps-2  38951  hlatexch3N  38953  llnle  38991  atcvrlln2  38992  atcvrlln  38993  lplni2  39010  lplnle  39013  lplnnle2at  39014  llncvrlpln2  39030  lplnexllnN  39037  2llnmeqat  39044  lvolnle3at  39055  4atlem0ae  39067  lplncvrlvol2  39088  lnjatN  39253  lncvrat  39255  cdlemblem  39266  elpaddri  39275  paddasslem2  39294  paddasslem16  39308  padd4N  39313  hlmod1i  39329  dalawlem2  39345  pclfinN  39373  pexmidlem4N  39446  pl42lem1N  39452  lhp2lt  39474  lhpexle1  39481  lhpexle2lem  39482  lhpj1  39495  lhpmcvr5N  39500  lhp2at0  39505  lhp2atnle  39506  lhp2at0nle  39508  lhple  39515  lhpat  39516  lhpat4N  39517  4atexlempnq  39528  4atexlem7  39548  4atex  39549  ltrn11  39599  ltrnle  39602  ltrnm  39604  ltrnj  39605  ltrncvr  39606  ltrnel  39612  ltrncnvel  39615  ltrncnv  39619  trlval2  39636  trlcnv  39638  trljat1  39639  trljat2  39640  trlat  39642  trl0  39643  trlnidat  39646  trlnid  39652  cdlemc1  39664  cdlemc2  39665  cdlemc5  39668  cdlemd2  39672  cdlemd7  39677  cdlemd8  39678  cdlemd9  39679  cdleme0e  39690  cdleme3g  39707  cdleme3h  39708  cdleme3  39710  cdleme5  39713  cdleme10  39727  cdleme11a  39733  cdleme11c  39734  cdleme11h  39739  cdleme11j  39740  cdleme0nex  39763  cdleme18a  39764  cdleme18b  39765  cdleme22gb  39767  cdleme20zN  39774  cdleme20c  39784  cdleme20k  39792  cdleme21a  39798  cdleme21b  39799  cdleme21c  39800  cdleme21h  39807  cdleme22b  39814  cdleme22d  39816  cdleme22f  39819  cdleme25a  39826  cdleme25c  39828  cdleme25dN  39829  cdleme26ee  39833  cdleme30a  39851  cdlemefr29bpre0N  39879  cdlemefr29clN  39880  cdlemefr32fvaN  39882  cdlemefr32fva1  39883  cdlemefs29bpre0N  39889  cdlemefs29bpre1N  39890  cdlemefs29cpre1N  39891  cdlemefs29clN  39892  cdleme43fsv1snlem  39893  cdlemefs32fvaN  39895  cdlemefs32fva1  39896  cdlemefs31fv1  39897  cdleme36a  39933  cdleme39a  39938  cdleme42a  39944  cdleme42c  39945  cdleme17d3  39969  cdleme48fv  39972  cdleme48bw  39975  cdleme48b  39976  cdlemeg46rgv  40001  cdlemeg46req  40002  cdlemeg46gfv  40003  cdleme48d  40008  cdleme50trn2a  40023  cdleme50trn2  40024  cdleme50ltrn  40030  cdlemf1  40034  cdlemf  40036  trlord  40042  cdlemg2dN  40063  cdlemg2fvlem  40067  cdlemg2l  40076  cdlemg7fvbwN  40080  cdlemg7aN  40098  cdlemg10bALTN  40109  cdlemg10c  40112  cdlemg17a  40134  cdlemg17dALTN  40137  cdlemg31b0a  40168  cdlemg31a  40170  cdlemg31b  40171  cdlemg34  40185  cdlemg36  40187  ltrnco  40192  trlcoabs2N  40195  trlcolem  40199  cdlemg48  40210  tgrpov  40221  tendoco2  40241  tendoplco2  40252  cdlemh1  40288  cdlemi1  40291  cdlemi2  40292  cdlemj3  40296  tendoid0  40298  cdlemk1  40304  cdlemk2  40305  cdlemk4  40307  cdlemk8  40311  cdlemk9  40312  cdlemk9bN  40313  cdlemk10  40316  cdlemk26b-3  40378  cdlemk26-3  40379  cdlemk28-3  40381  cdlemk37  40387  cdlemk39  40389  cdlemkfid1N  40394  cdlemkid1  40395  cdlemky  40399  cdlemkyu  40400  cdlemk19ylem  40403  cdlemk19xlem  40415  cdlemk11t  40419  cdlemk51  40426  cdlemkyyN  40435  cdleml6  40454  cdleml7  40455  cdleml8  40456  cdleml9  40457  erngdvlem4  40464  erngdvlem4-rN  40472  tendospcanN  40496  dia11N  40521  cdlemm10N  40591  dib11N  40633  dicvaddcl  40663  dicvscacl  40664  cdlemn6  40675  dihvalcq2  40720  dihopelvalcpre  40721  dihord6b  40733  dihord5apre  40735  dihmeetlem1N  40763  dihmeetlem2N  40772  dihglbcpreN  40773  dihjatc1  40784  dihmeetlem20N  40799  dih1dimatlem0  40801  dihatlat  40807  dihglblem6  40813  dochexmidlem4  40936  mapdpglem32  41178  mapdh8ad  41252  mapdh9aOLDN  41263  hdmap11lem2  41315  hdmap14lem6  41346  frlmfzowrdb  41744  flt4lem5  42074  mzpsubst  42168  pellex  42255  pellfundex  42306  pellfund14gap  42307  qirropth  42328  rmxypos  42368  congmul  42388  congsub  42391  mzpcong  42393  coprmdvdsb  42406  jm2.15nn0  42424  jm2.16nn0  42425  rpnnen3lem  42452  idomsubgmo  42621  relexp01min  43143  mullimc  45004  islptre  45007  limccog  45008  mullimcf  45011  addlimc  45036  0ellimcdiv  45037  limsupre3lem  45120  stoweidlem57  45445  fourierdlem48  45542  fourierdlem80  45574  fourierdlem113  45607  ovncvrrp  45952  opnvonmbllem2  46021  ovolval5lem3  46042  ovnovollem3  46046  itsclc0lem1  47829  itsclc0lem2  47830  itschlc0yqe  47833  itscnhlc0xyqsol  47838  itschlc0xyqsol1  47839