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  7852  fpr3g  8282  tfrlem5  8392  omeulem1  8592  omeulem2  8593  uniinqs  8809  elfiun  9440  tcrank  9896  isfin2-2  10331  konigthlem  10580  gruen  10824  addlid  11416  mulcan  11872  mulcan2  11873  divass  11912  divdir  11919  div11OLD  11923  muldivdir  11932  subdivcomb1  11934  subdivcomb2  11935  divcan5  11941  ltmul1  12089  ltdiv1  12104  ltmuldiv  12113  lediv2  12130  xaddass2  13264  xlt2add  13274  xmulasslem3  13300  xadddi2  13311  expaddz  14122  expmulz  14124  muldivbinom2  14279  resqrtcl  15270  o1add  15628  o1mul  15629  o1sub  15630  dvdsadd2b  16323  dvdsgcd  16561  rpexp12i  16741  pythagtriplem3  16836  pcpremul  16861  pceu  16864  pcqmul  16871  pcqdiv  16875  setsstruct  17193  f1ocpbllem  17536  funcoppc  17886  funcres  17907  catcisolem  18121  1stfcl  18207  2ndfcl  18208  prfcl  18213  evlfcl  18232  curf1cl  18238  curfcl  18242  hofcl  18269  latjlej12  18463  latmlem12  18479  latj4  18497  latj4rot  18498  symgsssg  19446  symgfisg  19447  psgnunilem4  19476  odcong  19528  cmn4  19780  ablsub4  19789  abladdsub4  19790  lsm4  19839  abvdom  20788  abvres  20789  abvtrivd  20790  lspsolvlem  21101  lbsextlem2  21118  lidlsubcl  21183  frlmbas3  21734  matmulcell  22381  marrepeval  22499  ma1repveval  22507  submaeval  22518  mdetunilem3  22550  mdetuni0  22557  mdetmul  22559  minmar1eval  22585  nllyrest  23422  hausflimlem  23915  tsmsxp  24091  psmetlecl  24252  xmetlecl  24283  prdsxmetlem  24305  ngpocelbl  24641  bndth  24906  cph2ass  25163  iscau3  25228  dvres2  25863  coemullem  26205  vieta1  26270  aalioulem4  26293  cxpcn3lem  26707  angcan  26762  dchrvmasumlema  27461  logdivsum  27494  abvcxp  27576  padicabv  27591  nosupbnd1lem4  27673  nosupbnd1lem5  27674  noinfbnd1lem4  27688  cofcut1  27871  cofcut2  27873  divsmulw  28135  precsexlem8  28155  precsexlem9  28156  ax5seglem3  28856  ax5seglem6  28859  axpasch  28866  axeuclid  28888  axcontlem4  28892  axcontlem8  28896  wlkl1loop  29564  trlsonwlkon  29636  pthontrlon  29675  wspthsswwlknon  29849  frgr2wwlkeqm  30258  adjlnop  32013  xreceu  32842  orngmul  33271  rhmdvd  33286  measvunilem  34189  measvunilem0  34190  measres  34199  bnj1128  34967  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  37733  heibor  37791  lsmcv2  38993  lcvat  38994  lcvexchlem4  39001  lcvexchlem5  39002  lfladd  39030  lflsub  39031  lflmul  39032  lshpkrlem4  39077  latm4  39197  omlmod1i2N  39224  cvlatexch3  39302  cvlsupr7  39312  hlatj4  39338  hlrelat3  39377  cvrval3  39378  atcvrj1  39396  atlelt  39403  2atlt  39404  2atjm  39410  3noncolr2  39414  athgt  39421  3dimlem2  39424  3dimlem4  39429  3dimlem4OLDN  39430  3dim3  39434  1cvratex  39438  ps-1  39442  ps-2  39443  hlatexch3N  39445  llnle  39483  atcvrlln2  39484  atcvrlln  39485  lplni2  39502  lplnle  39505  lplnnle2at  39506  llncvrlpln2  39522  lplnexllnN  39529  2llnmeqat  39536  lvolnle3at  39547  4atlem0ae  39559  lplncvrlvol2  39580  lnjatN  39745  lncvrat  39747  cdlemblem  39758  elpaddri  39767  paddasslem2  39786  paddasslem16  39800  padd4N  39805  hlmod1i  39821  dalawlem2  39837  pclfinN  39865  pexmidlem4N  39938  pl42lem1N  39944  lhp2lt  39966  lhpexle1  39973  lhpexle2lem  39974  lhpj1  39987  lhpmcvr5N  39992  lhp2at0  39997  lhp2atnle  39998  lhp2at0nle  40000  lhple  40007  lhpat  40008  lhpat4N  40009  4atexlempnq  40020  4atexlem7  40040  4atex  40041  ltrn11  40091  ltrnle  40094  ltrnm  40096  ltrnj  40097  ltrncvr  40098  ltrnel  40104  ltrncnvel  40107  ltrncnv  40111  trlval2  40128  trlcnv  40130  trljat1  40131  trljat2  40132  trlat  40134  trl0  40135  trlnidat  40138  trlnid  40144  cdlemc1  40156  cdlemc2  40157  cdlemc5  40160  cdlemd2  40164  cdlemd7  40169  cdlemd8  40170  cdlemd9  40171  cdleme0e  40182  cdleme3g  40199  cdleme3h  40200  cdleme3  40202  cdleme5  40205  cdleme10  40219  cdleme11a  40225  cdleme11c  40226  cdleme11h  40231  cdleme11j  40232  cdleme0nex  40255  cdleme18a  40256  cdleme18b  40257  cdleme22gb  40259  cdleme20zN  40266  cdleme20c  40276  cdleme20k  40284  cdleme21a  40290  cdleme21b  40291  cdleme21c  40292  cdleme21h  40299  cdleme22b  40306  cdleme22d  40308  cdleme22f  40311  cdleme25a  40318  cdleme25c  40320  cdleme25dN  40321  cdleme26ee  40325  cdleme30a  40343  cdlemefr29bpre0N  40371  cdlemefr29clN  40372  cdlemefr32fvaN  40374  cdlemefr32fva1  40375  cdlemefs29bpre0N  40381  cdlemefs29bpre1N  40382  cdlemefs29cpre1N  40383  cdlemefs29clN  40384  cdleme43fsv1snlem  40385  cdlemefs32fvaN  40387  cdlemefs32fva1  40388  cdlemefs31fv1  40389  cdleme36a  40425  cdleme39a  40430  cdleme42a  40436  cdleme42c  40437  cdleme17d3  40461  cdleme48fv  40464  cdleme48bw  40467  cdleme48b  40468  cdlemeg46rgv  40493  cdlemeg46req  40494  cdlemeg46gfv  40495  cdleme48d  40500  cdleme50trn2a  40515  cdleme50trn2  40516  cdleme50ltrn  40522  cdlemf1  40526  cdlemf  40528  trlord  40534  cdlemg2dN  40555  cdlemg2fvlem  40559  cdlemg2l  40568  cdlemg7fvbwN  40572  cdlemg7aN  40590  cdlemg10bALTN  40601  cdlemg10c  40604  cdlemg17a  40626  cdlemg17dALTN  40629  cdlemg31b0a  40660  cdlemg31a  40662  cdlemg31b  40663  cdlemg34  40677  cdlemg36  40679  ltrnco  40684  trlcoabs2N  40687  trlcolem  40691  cdlemg48  40702  tgrpov  40713  tendoco2  40733  tendoplco2  40744  cdlemh1  40780  cdlemi1  40783  cdlemi2  40784  cdlemj3  40788  tendoid0  40790  cdlemk1  40796  cdlemk2  40797  cdlemk4  40799  cdlemk8  40803  cdlemk9  40804  cdlemk9bN  40805  cdlemk10  40808  cdlemk26b-3  40870  cdlemk26-3  40871  cdlemk28-3  40873  cdlemk37  40879  cdlemk39  40881  cdlemkfid1N  40886  cdlemkid1  40887  cdlemky  40891  cdlemkyu  40892  cdlemk19ylem  40895  cdlemk19xlem  40907  cdlemk11t  40911  cdlemk51  40918  cdlemkyyN  40927  cdleml6  40946  cdleml7  40947  cdleml8  40948  cdleml9  40949  erngdvlem4  40956  erngdvlem4-rN  40964  tendospcanN  40988  dia11N  41013  cdlemm10N  41083  dib11N  41125  dicvaddcl  41155  dicvscacl  41156  cdlemn6  41167  dihvalcq2  41212  dihopelvalcpre  41213  dihord6b  41225  dihord5apre  41227  dihmeetlem1N  41255  dihmeetlem2N  41264  dihglbcpreN  41265  dihjatc1  41276  dihmeetlem20N  41291  dih1dimatlem0  41293  dihatlat  41299  dihglblem6  41305  dochexmidlem4  41428  mapdpglem32  41670  mapdh8ad  41744  mapdh9aOLDN  41755  hdmap11lem2  41807  hdmap14lem6  41838  frlmfzowrdb  42474  flt4lem5  42620  mzpsubst  42718  pellex  42805  pellfundex  42856  pellfund14gap  42857  qirropth  42878  rmxypos  42918  congmul  42938  congsub  42941  mzpcong  42943  coprmdvdsb  42956  jm2.15nn0  42974  jm2.16nn0  42975  rpnnen3lem  43002  idomsubgmo  43164  relexp01min  43684  mullimc  45593  islptre  45596  limccog  45597  mullimcf  45600  addlimc  45625  0ellimcdiv  45626  limsupre3lem  45709  stoweidlem57  46034  fourierdlem48  46131  fourierdlem80  46163  fourierdlem113  46196  ovncvrrp  46541  opnvonmbllem2  46610  ovolval5lem3  46631  ovnovollem3  46635  itsclc0lem1  48684  itsclc0lem2  48685  itschlc0yqe  48688  itscnhlc0xyqsol  48693  itschlc0xyqsol1  48694  swapffunc  49147  fucofunc  49218