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

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

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 1089

This theorem is referenced by:  simp13l  1289  simp23l  1295  simp33l  1301  tfisi  7880  fpr3g  8310  tfrlem5  8420  omeulem1  8620  omeulem2  8621  uniinqs  8837  elfiun  9470  tcrank  9924  isfin2-2  10359  konigthlem  10608  gruen  10852  addlid  11444  mulcan  11900  mulcan2  11901  divass  11940  divdir  11947  div11OLD  11951  muldivdir  11960  subdivcomb1  11962  subdivcomb2  11963  divcan5  11969  ltmul1  12117  ltdiv1  12132  ltmuldiv  12141  lediv2  12158  xaddass2  13292  xlt2add  13302  xmulasslem3  13328  xadddi2  13339  expaddz  14147  expmulz  14149  muldivbinom2  14302  resqrtcl  15292  o1add  15650  o1mul  15651  o1sub  15652  dvdsadd2b  16343  dvdsgcd  16581  rpexp12i  16761  pythagtriplem3  16856  pcpremul  16881  pceu  16884  pcqmul  16891  pcqdiv  16895  setsstruct  17213  f1ocpbllem  17569  funcoppc  17920  funcres  17941  catcisolem  18155  1stfcl  18242  2ndfcl  18243  prfcl  18248  evlfcl  18267  curf1cl  18273  curfcl  18277  hofcl  18304  latjlej12  18500  latmlem12  18516  latj4  18534  latj4rot  18535  symgsssg  19485  symgfisg  19486  psgnunilem4  19515  odcong  19567  cmn4  19819  ablsub4  19828  abladdsub4  19829  lsm4  19878  abvdom  20831  abvres  20832  abvtrivd  20833  lspsolvlem  21144  lbsextlem2  21161  lidlsubcl  21234  frlmbas3  21796  matmulcell  22451  marrepeval  22569  ma1repveval  22577  submaeval  22588  mdetunilem3  22620  mdetuni0  22627  mdetmul  22629  minmar1eval  22655  nllyrest  23494  hausflimlem  23987  tsmsxp  24163  psmetlecl  24325  xmetlecl  24356  prdsxmetlem  24378  ngpocelbl  24725  bndth  24990  cph2ass  25247  iscau3  25312  dvres2  25947  coemullem  26289  vieta1  26354  aalioulem4  26377  cxpcn3lem  26790  angcan  26845  dchrvmasumlema  27544  logdivsum  27577  abvcxp  27659  padicabv  27674  nosupbnd1lem4  27756  nosupbnd1lem5  27757  noinfbnd1lem4  27771  cofcut1  27954  cofcut2  27956  divsmulw  28218  precsexlem8  28238  precsexlem9  28239  ax5seglem3  28946  ax5seglem6  28949  axpasch  28956  axeuclid  28978  axcontlem4  28982  axcontlem8  28986  wlkl1loop  29656  trlsonwlkon  29728  pthontrlon  29767  wspthsswwlknon  29941  frgr2wwlkeqm  30350  adjlnop  32105  xreceu  32904  orngmul  33333  rhmdvd  33348  measvunilem  34213  measvunilem0  34214  measres  34223  bnj1128  35004  umgr2cycllem  35145  umgr2cycl  35146  satfv1fvfmla1  35428  cgrcomim  35990  cgrcoml  35997  cgrcomr  35998  cgrdegen  36005  segconeu  36012  btwnintr  36020  btwnexch3  36021  btwnouttr2  36023  btwnouttr  36025  btwnexch  36026  trisegint  36029  lineext  36077  linecgr  36082  lineid  36084  idinside  36085  btwnconn1lem3  36090  btwnconn1lem4  36091  btwnconn1lem7  36094  btwnconn1lem14  36101  btwnconn2  36103  midofsegid  36105  btwnoutside  36126  outsideoftr  36130  lineunray  36148  lineelsb2  36149  cnres2  37770  heibor  37828  lsmcv2  39030  lcvat  39031  lcvexchlem4  39038  lcvexchlem5  39039  lfladd  39067  lflsub  39068  lflmul  39069  lshpkrlem4  39114  latm4  39234  omlmod1i2N  39261  cvlatexch3  39339  cvlsupr7  39349  hlatj4  39375  hlrelat3  39414  cvrval3  39415  atcvrj1  39433  atlelt  39440  2atlt  39441  2atjm  39447  3noncolr2  39451  athgt  39458  3dimlem2  39461  3dimlem4  39466  3dimlem4OLDN  39467  3dim3  39471  1cvratex  39475  ps-1  39479  ps-2  39480  hlatexch3N  39482  llnle  39520  atcvrlln2  39521  atcvrlln  39522  lplni2  39539  lplnle  39542  lplnnle2at  39543  llncvrlpln2  39559  lplnexllnN  39566  2llnmeqat  39573  lvolnle3at  39584  4atlem0ae  39596  lplncvrlvol2  39617  lnjatN  39782  lncvrat  39784  cdlemblem  39795  elpaddri  39804  paddasslem2  39823  paddasslem16  39837  padd4N  39842  hlmod1i  39858  dalawlem2  39874  pclfinN  39902  pexmidlem4N  39975  pl42lem1N  39981  lhp2lt  40003  lhpexle1  40010  lhpexle2lem  40011  lhpj1  40024  lhpmcvr5N  40029  lhp2at0  40034  lhp2atnle  40035  lhp2at0nle  40037  lhple  40044  lhpat  40045  lhpat4N  40046  4atexlempnq  40057  4atexlem7  40077  4atex  40078  ltrn11  40128  ltrnle  40131  ltrnm  40133  ltrnj  40134  ltrncvr  40135  ltrnel  40141  ltrncnvel  40144  ltrncnv  40148  trlval2  40165  trlcnv  40167  trljat1  40168  trljat2  40169  trlat  40171  trl0  40172  trlnidat  40175  trlnid  40181  cdlemc1  40193  cdlemc2  40194  cdlemc5  40197  cdlemd2  40201  cdlemd7  40206  cdlemd8  40207  cdlemd9  40208  cdleme0e  40219  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme5  40242  cdleme10  40256  cdleme11a  40262  cdleme11c  40263  cdleme11h  40268  cdleme11j  40269  cdleme0nex  40292  cdleme18a  40293  cdleme18b  40294  cdleme22gb  40296  cdleme20zN  40303  cdleme20c  40313  cdleme20k  40321  cdleme21a  40327  cdleme21b  40328  cdleme21c  40329  cdleme21h  40336  cdleme22b  40343  cdleme22d  40345  cdleme22f  40348  cdleme25a  40355  cdleme25c  40357  cdleme25dN  40358  cdleme26ee  40362  cdleme30a  40380  cdlemefr29bpre0N  40408  cdlemefr29clN  40409  cdlemefr32fvaN  40411  cdlemefr32fva1  40412  cdlemefs29bpre0N  40418  cdlemefs29bpre1N  40419  cdlemefs29cpre1N  40420  cdlemefs29clN  40421  cdleme43fsv1snlem  40422  cdlemefs32fvaN  40424  cdlemefs32fva1  40425  cdlemefs31fv1  40426  cdleme36a  40462  cdleme39a  40467  cdleme42a  40473  cdleme42c  40474  cdleme17d3  40498  cdleme48fv  40501  cdleme48bw  40504  cdleme48b  40505  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemeg46gfv  40532  cdleme48d  40537  cdleme50trn2a  40552  cdleme50trn2  40553  cdleme50ltrn  40559  cdlemf1  40563  cdlemf  40565  trlord  40571  cdlemg2dN  40592  cdlemg2fvlem  40596  cdlemg2l  40605  cdlemg7fvbwN  40609  cdlemg7aN  40627  cdlemg10bALTN  40638  cdlemg10c  40641  cdlemg17a  40663  cdlemg17dALTN  40666  cdlemg31b0a  40697  cdlemg31a  40699  cdlemg31b  40700  cdlemg34  40714  cdlemg36  40716  ltrnco  40721  trlcoabs2N  40724  trlcolem  40728  cdlemg48  40739  tgrpov  40750  tendoco2  40770  tendoplco2  40781  cdlemh1  40817  cdlemi1  40820  cdlemi2  40821  cdlemj3  40825  tendoid0  40827  cdlemk1  40833  cdlemk2  40834  cdlemk4  40836  cdlemk8  40840  cdlemk9  40841  cdlemk9bN  40842  cdlemk10  40845  cdlemk26b-3  40907  cdlemk26-3  40908  cdlemk28-3  40910  cdlemk37  40916  cdlemk39  40918  cdlemkfid1N  40923  cdlemkid1  40924  cdlemky  40928  cdlemkyu  40929  cdlemk19ylem  40932  cdlemk19xlem  40944  cdlemk11t  40948  cdlemk51  40955  cdlemkyyN  40964  cdleml6  40983  cdleml7  40984  cdleml8  40985  cdleml9  40986  erngdvlem4  40993  erngdvlem4-rN  41001  tendospcanN  41025  dia11N  41050  cdlemm10N  41120  dib11N  41162  dicvaddcl  41192  dicvscacl  41193  cdlemn6  41204  dihvalcq2  41249  dihopelvalcpre  41250  dihord6b  41262  dihord5apre  41264  dihmeetlem1N  41292  dihmeetlem2N  41301  dihglbcpreN  41302  dihjatc1  41313  dihmeetlem20N  41328  dih1dimatlem0  41330  dihatlat  41336  dihglblem6  41342  dochexmidlem4  41465  mapdpglem32  41707  mapdh8ad  41781  mapdh9aOLDN  41792  hdmap11lem2  41844  hdmap14lem6  41875  frlmfzowrdb  42514  flt4lem5  42660  mzpsubst  42759  pellex  42846  pellfundex  42897  pellfund14gap  42898  qirropth  42919  rmxypos  42959  congmul  42979  congsub  42982  mzpcong  42984  coprmdvdsb  42997  jm2.15nn0  43015  jm2.16nn0  43016  rpnnen3lem  43043  idomsubgmo  43205  relexp01min  43726  mullimc  45631  islptre  45634  limccog  45635  mullimcf  45638  addlimc  45663  0ellimcdiv  45664  limsupre3lem  45747  stoweidlem57  46072  fourierdlem48  46169  fourierdlem80  46201  fourierdlem113  46234  ovncvrrp  46579  opnvonmbllem2  46648  ovolval5lem3  46669  ovnovollem3  46673  itsclc0lem1  48677  itsclc0lem2  48678  itschlc0yqe  48681  itscnhlc0xyqsol  48686  itschlc0xyqsol1  48687  swapffunc  48988  fucofunc  49054