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  7789  fpr3g  8215  tfrlem5  8299  omeulem1  8497  omeulem2  8498  uniinqs  8721  elfiun  9314  tcrank  9774  isfin2-2  10207  konigthlem  10456  gruen  10700  addlid  11293  mulcan  11751  mulcan2  11752  divass  11791  divdir  11798  div11OLD  11802  muldivdir  11811  subdivcomb1  11813  subdivcomb2  11814  divcan5  11820  ltmul1  11968  ltdiv1  11983  ltmuldiv  11992  lediv2  12009  xaddass2  13146  xlt2add  13156  xmulasslem3  13182  xadddi2  13193  expaddz  14010  expmulz  14012  muldivbinom2  14167  resqrtcl  15157  o1add  15518  o1mul  15519  o1sub  15520  dvdsadd2b  16214  dvdsgcd  16452  rpexp12i  16632  pythagtriplem3  16727  pcpremul  16752  pceu  16755  pcqmul  16762  pcqdiv  16766  setsstruct  17084  f1ocpbllem  17425  funcoppc  17779  funcres  17800  catcisolem  18014  1stfcl  18100  2ndfcl  18101  prfcl  18106  evlfcl  18125  curf1cl  18131  curfcl  18135  hofcl  18162  latjlej12  18358  latmlem12  18374  latj4  18392  latj4rot  18393  symgsssg  19377  symgfisg  19378  psgnunilem4  19407  odcong  19459  cmn4  19711  ablsub4  19720  abladdsub4  19721  lsm4  19770  abvdom  20743  abvres  20744  abvtrivd  20745  orngmul  20778  lspsolvlem  21077  lbsextlem2  21094  lidlsubcl  21159  frlmbas3  21711  matmulcell  22358  marrepeval  22476  ma1repveval  22484  submaeval  22495  mdetunilem3  22527  mdetuni0  22534  mdetmul  22536  minmar1eval  22562  nllyrest  23399  hausflimlem  23892  tsmsxp  24068  psmetlecl  24228  xmetlecl  24259  prdsxmetlem  24281  ngpocelbl  24617  bndth  24882  cph2ass  25138  iscau3  25203  dvres2  25838  coemullem  26180  vieta1  26245  aalioulem4  26268  cxpcn3lem  26682  angcan  26737  dchrvmasumlema  27436  logdivsum  27469  abvcxp  27551  padicabv  27566  nosupbnd1lem4  27648  nosupbnd1lem5  27649  noinfbnd1lem4  27663  cofcut1  27862  cofcut2  27864  divsmulw  28130  precsexlem8  28150  precsexlem9  28151  ax5seglem3  28907  ax5seglem6  28910  axpasch  28917  axeuclid  28939  axcontlem4  28943  axcontlem8  28947  wlkl1loop  29614  trlsonwlkon  29684  pthontrlon  29723  wspthsswwlknon  29897  frgr2wwlkeqm  30306  adjlnop  32061  xreceu  32897  rhmdvd  33284  measvunilem  34220  measvunilem0  34221  measres  34230  bnj1128  34997  umgr2cycllem  35172  umgr2cycl  35173  satfv1fvfmla1  35455  cgrcomim  36022  cgrcoml  36029  cgrcomr  36030  cgrdegen  36037  segconeu  36044  btwnintr  36052  btwnexch3  36053  btwnouttr2  36055  btwnouttr  36057  btwnexch  36058  trisegint  36061  lineext  36109  linecgr  36114  lineid  36116  idinside  36117  btwnconn1lem3  36122  btwnconn1lem4  36123  btwnconn1lem7  36126  btwnconn1lem14  36133  btwnconn2  36135  midofsegid  36137  btwnoutside  36158  outsideoftr  36162  lineunray  36180  lineelsb2  36181  cnres2  37802  heibor  37860  lsmcv2  39067  lcvat  39068  lcvexchlem4  39075  lcvexchlem5  39076  lfladd  39104  lflsub  39105  lflmul  39106  lshpkrlem4  39151  latm4  39271  omlmod1i2N  39298  cvlatexch3  39376  cvlsupr7  39386  hlatj4  39412  hlrelat3  39450  cvrval3  39451  atcvrj1  39469  atlelt  39476  2atlt  39477  2atjm  39483  3noncolr2  39487  athgt  39494  3dimlem2  39497  3dimlem4  39502  3dimlem4OLDN  39503  3dim3  39507  1cvratex  39511  ps-1  39515  ps-2  39516  hlatexch3N  39518  llnle  39556  atcvrlln2  39557  atcvrlln  39558  lplni2  39575  lplnle  39578  lplnnle2at  39579  llncvrlpln2  39595  lplnexllnN  39602  2llnmeqat  39609  lvolnle3at  39620  4atlem0ae  39632  lplncvrlvol2  39653  lnjatN  39818  lncvrat  39820  cdlemblem  39831  elpaddri  39840  paddasslem2  39859  paddasslem16  39873  padd4N  39878  hlmod1i  39894  dalawlem2  39910  pclfinN  39938  pexmidlem4N  40011  pl42lem1N  40017  lhp2lt  40039  lhpexle1  40046  lhpexle2lem  40047  lhpj1  40060  lhpmcvr5N  40065  lhp2at0  40070  lhp2atnle  40071  lhp2at0nle  40073  lhple  40080  lhpat  40081  lhpat4N  40082  4atexlempnq  40093  4atexlem7  40113  4atex  40114  ltrn11  40164  ltrnle  40167  ltrnm  40169  ltrnj  40170  ltrncvr  40171  ltrnel  40177  ltrncnvel  40180  ltrncnv  40184  trlval2  40201  trlcnv  40203  trljat1  40204  trljat2  40205  trlat  40207  trl0  40208  trlnidat  40211  trlnid  40217  cdlemc1  40229  cdlemc2  40230  cdlemc5  40233  cdlemd2  40237  cdlemd7  40242  cdlemd8  40243  cdlemd9  40244  cdleme0e  40255  cdleme3g  40272  cdleme3h  40273  cdleme3  40275  cdleme5  40278  cdleme10  40292  cdleme11a  40298  cdleme11c  40299  cdleme11h  40304  cdleme11j  40305  cdleme0nex  40328  cdleme18a  40329  cdleme18b  40330  cdleme22gb  40332  cdleme20zN  40339  cdleme20c  40349  cdleme20k  40357  cdleme21a  40363  cdleme21b  40364  cdleme21c  40365  cdleme21h  40372  cdleme22b  40379  cdleme22d  40381  cdleme22f  40384  cdleme25a  40391  cdleme25c  40393  cdleme25dN  40394  cdleme26ee  40398  cdleme30a  40416  cdlemefr29bpre0N  40444  cdlemefr29clN  40445  cdlemefr32fvaN  40447  cdlemefr32fva1  40448  cdlemefs29bpre0N  40454  cdlemefs29bpre1N  40455  cdlemefs29cpre1N  40456  cdlemefs29clN  40457  cdleme43fsv1snlem  40458  cdlemefs32fvaN  40460  cdlemefs32fva1  40461  cdlemefs31fv1  40462  cdleme36a  40498  cdleme39a  40503  cdleme42a  40509  cdleme42c  40510  cdleme17d3  40534  cdleme48fv  40537  cdleme48bw  40540  cdleme48b  40541  cdlemeg46rgv  40566  cdlemeg46req  40567  cdlemeg46gfv  40568  cdleme48d  40573  cdleme50trn2a  40588  cdleme50trn2  40589  cdleme50ltrn  40595  cdlemf1  40599  cdlemf  40601  trlord  40607  cdlemg2dN  40628  cdlemg2fvlem  40632  cdlemg2l  40641  cdlemg7fvbwN  40645  cdlemg7aN  40663  cdlemg10bALTN  40674  cdlemg10c  40677  cdlemg17a  40699  cdlemg17dALTN  40702  cdlemg31b0a  40733  cdlemg31a  40735  cdlemg31b  40736  cdlemg34  40750  cdlemg36  40752  ltrnco  40757  trlcoabs2N  40760  trlcolem  40764  cdlemg48  40775  tgrpov  40786  tendoco2  40806  tendoplco2  40817  cdlemh1  40853  cdlemi1  40856  cdlemi2  40857  cdlemj3  40861  tendoid0  40863  cdlemk1  40869  cdlemk2  40870  cdlemk4  40872  cdlemk8  40876  cdlemk9  40877  cdlemk9bN  40878  cdlemk10  40881  cdlemk26b-3  40943  cdlemk26-3  40944  cdlemk28-3  40946  cdlemk37  40952  cdlemk39  40954  cdlemkfid1N  40959  cdlemkid1  40960  cdlemky  40964  cdlemkyu  40965  cdlemk19ylem  40968  cdlemk19xlem  40980  cdlemk11t  40984  cdlemk51  40991  cdlemkyyN  41000  cdleml6  41019  cdleml7  41020  cdleml8  41021  cdleml9  41022  erngdvlem4  41029  erngdvlem4-rN  41037  tendospcanN  41061  dia11N  41086  cdlemm10N  41156  dib11N  41198  dicvaddcl  41228  dicvscacl  41229  cdlemn6  41240  dihvalcq2  41285  dihopelvalcpre  41286  dihord6b  41298  dihord5apre  41300  dihmeetlem1N  41328  dihmeetlem2N  41337  dihglbcpreN  41338  dihjatc1  41349  dihmeetlem20N  41364  dih1dimatlem0  41366  dihatlat  41372  dihglblem6  41378  dochexmidlem4  41501  mapdpglem32  41743  mapdh8ad  41817  mapdh9aOLDN  41828  hdmap11lem2  41880  hdmap14lem6  41911  frlmfzowrdb  42536  flt4lem5  42682  mzpsubst  42780  pellex  42867  pellfundex  42918  pellfund14gap  42919  qirropth  42940  rmxypos  42979  congmul  42999  congsub  43002  mzpcong  43004  coprmdvdsb  43017  jm2.15nn0  43035  jm2.16nn0  43036  rpnnen3lem  43063  idomsubgmo  43225  relexp01min  43745  mullimc  45655  islptre  45658  limccog  45659  mullimcf  45662  addlimc  45685  0ellimcdiv  45686  limsupre3lem  45769  stoweidlem57  46094  fourierdlem48  46191  fourierdlem80  46223  fourierdlem113  46256  ovncvrrp  46601  opnvonmbllem2  46670  ovolval5lem3  46691  ovnovollem3  46695  grlimedgclnbgr  48025  itsclc0lem1  48787  itsclc0lem2  48788  itschlc0yqe  48791  itscnhlc0xyqsol  48796  itschlc0xyqsol1  48797  swapffunc  49313  fucofunc  49390  fucoppc  49441