Theorem simp3l 1203

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  1290  simp23l  1296  simp33l  1302  tfisi  7810  fpr3g  8235  tfrlem5  8319  omeulem1  8517  omeulem2  8518  uniinqs  8744  elfiun  9343  tcrank  9808  isfin2-2  10241  konigthlem  10491  gruen  10735  addlid  11329  mulcan  11787  mulcan2  11788  divass  11827  divdir  11834  div11OLD  11838  muldivdir  11847  subdivcomb1  11850  subdivcomb2  11851  divcan5  11857  ltmul1  12005  ltdiv1  12020  ltmuldiv  12029  lediv2  12046  xaddass2  13202  xlt2add  13212  xmulasslem3  13238  xadddi2  13249  expaddz  14068  expmulz  14070  muldivbinom2  14225  resqrtcl  15215  o1add  15576  o1mul  15577  o1sub  15578  dvdsadd2b  16275  dvdsgcd  16513  rpexp12i  16694  pythagtriplem3  16789  pcpremul  16814  pceu  16817  pcqmul  16824  pcqdiv  16828  setsstruct  17146  f1ocpbllem  17488  funcoppc  17842  funcres  17863  catcisolem  18077  1stfcl  18163  2ndfcl  18164  prfcl  18169  evlfcl  18188  curf1cl  18194  curfcl  18198  hofcl  18225  latjlej12  18421  latmlem12  18437  latj4  18455  latj4rot  18456  symgsssg  19442  symgfisg  19443  psgnunilem4  19472  odcong  19524  cmn4  19776  ablsub4  19785  abladdsub4  19786  lsm4  19835  abvdom  20807  abvres  20808  abvtrivd  20809  orngmul  20842  lspsolvlem  21140  lbsextlem2  21157  lidlsubcl  21222  frlmbas3  21756  matmulcell  22410  marrepeval  22528  ma1repveval  22536  submaeval  22547  mdetunilem3  22579  mdetuni0  22586  mdetmul  22588  minmar1eval  22614  nllyrest  23451  hausflimlem  23944  tsmsxp  24120  psmetlecl  24280  xmetlecl  24311  prdsxmetlem  24333  ngpocelbl  24669  bndth  24925  cph2ass  25180  iscau3  25245  dvres2  25879  coemullem  26215  vieta1  26278  aalioulem4  26301  cxpcn3lem  26711  angcan  26766  dchrvmasumlema  27463  logdivsum  27496  abvcxp  27578  padicabv  27593  nosupbnd1lem4  27675  nosupbnd1lem5  27676  noinfbnd1lem4  27690  cofcut1  27912  cofcut2  27914  divmulsw  28185  precsexlem8  28206  precsexlem9  28207  bdayfinbndlem1  28459  ax5seglem3  29000  ax5seglem6  29003  axpasch  29010  axeuclid  29032  axcontlem4  29036  axcontlem8  29040  wlkl1loop  29706  trlsonwlkon  29776  pthontrlon  29815  wspthsswwlknon  29989  frgr2wwlkeqm  30401  adjlnop  32157  xreceu  32981  rhmdvd  33384  measvunilem  34356  measvunilem0  34357  measres  34366  bnj1128  35132  umgr2cycllem  35322  umgr2cycl  35323  satfv1fvfmla1  35605  cgrcomim  36171  cgrcoml  36178  cgrcomr  36179  cgrdegen  36186  segconeu  36193  btwnintr  36201  btwnexch3  36202  btwnouttr2  36204  btwnouttr  36206  btwnexch  36207  trisegint  36210  lineext  36258  linecgr  36263  lineid  36265  idinside  36266  btwnconn1lem3  36271  btwnconn1lem4  36272  btwnconn1lem7  36275  btwnconn1lem14  36282  btwnconn2  36284  midofsegid  36286  btwnoutside  36307  outsideoftr  36311  lineunray  36329  lineelsb2  36330  cnres2  38084  heibor  38142  lsmcv2  39475  lcvat  39476  lcvexchlem4  39483  lcvexchlem5  39484  lfladd  39512  lflsub  39513  lflmul  39514  lshpkrlem4  39559  latm4  39679  omlmod1i2N  39706  cvlatexch3  39784  cvlsupr7  39794  hlatj4  39820  hlrelat3  39858  cvrval3  39859  atcvrj1  39877  atlelt  39884  2atlt  39885  2atjm  39891  3noncolr2  39895  athgt  39902  3dimlem2  39905  3dimlem4  39910  3dimlem4OLDN  39911  3dim3  39915  1cvratex  39919  ps-1  39923  ps-2  39924  hlatexch3N  39926  llnle  39964  atcvrlln2  39965  atcvrlln  39966  lplni2  39983  lplnle  39986  lplnnle2at  39987  llncvrlpln2  40003  lplnexllnN  40010  2llnmeqat  40017  lvolnle3at  40028  4atlem0ae  40040  lplncvrlvol2  40061  lnjatN  40226  lncvrat  40228  cdlemblem  40239  elpaddri  40248  paddasslem2  40267  paddasslem16  40281  padd4N  40286  hlmod1i  40302  dalawlem2  40318  pclfinN  40346  pexmidlem4N  40419  pl42lem1N  40425  lhp2lt  40447  lhpexle1  40454  lhpexle2lem  40455  lhpj1  40468  lhpmcvr5N  40473  lhp2at0  40478  lhp2atnle  40479  lhp2at0nle  40481  lhple  40488  lhpat  40489  lhpat4N  40490  4atexlempnq  40501  4atexlem7  40521  4atex  40522  ltrn11  40572  ltrnle  40575  ltrnm  40577  ltrnj  40578  ltrncvr  40579  ltrnel  40585  ltrncnvel  40588  ltrncnv  40592  trlval2  40609  trlcnv  40611  trljat1  40612  trljat2  40613  trlat  40615  trl0  40616  trlnidat  40619  trlnid  40625  cdlemc1  40637  cdlemc2  40638  cdlemc5  40641  cdlemd2  40645  cdlemd7  40650  cdlemd8  40651  cdlemd9  40652  cdleme0e  40663  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme5  40686  cdleme10  40700  cdleme11a  40706  cdleme11c  40707  cdleme11h  40712  cdleme11j  40713  cdleme0nex  40736  cdleme18a  40737  cdleme18b  40738  cdleme22gb  40740  cdleme20zN  40747  cdleme20c  40757  cdleme20k  40765  cdleme21a  40771  cdleme21b  40772  cdleme21c  40773  cdleme21h  40780  cdleme22b  40787  cdleme22d  40789  cdleme22f  40792  cdleme25a  40799  cdleme25c  40801  cdleme25dN  40802  cdleme26ee  40806  cdleme30a  40824  cdlemefr29bpre0N  40852  cdlemefr29clN  40853  cdlemefr32fvaN  40855  cdlemefr32fva1  40856  cdlemefs29bpre0N  40862  cdlemefs29bpre1N  40863  cdlemefs29cpre1N  40864  cdlemefs29clN  40865  cdleme43fsv1snlem  40866  cdlemefs32fvaN  40868  cdlemefs32fva1  40869  cdlemefs31fv1  40870  cdleme36a  40906  cdleme39a  40911  cdleme42a  40917  cdleme42c  40918  cdleme17d3  40942  cdleme48fv  40945  cdleme48bw  40948  cdleme48b  40949  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemeg46gfv  40976  cdleme48d  40981  cdleme50trn2a  40996  cdleme50trn2  40997  cdleme50ltrn  41003  cdlemf1  41007  cdlemf  41009  trlord  41015  cdlemg2dN  41036  cdlemg2fvlem  41040  cdlemg2l  41049  cdlemg7fvbwN  41053  cdlemg7aN  41071  cdlemg10bALTN  41082  cdlemg10c  41085  cdlemg17a  41107  cdlemg17dALTN  41110  cdlemg31b0a  41141  cdlemg31a  41143  cdlemg31b  41144  cdlemg34  41158  cdlemg36  41160  ltrnco  41165  trlcoabs2N  41168  trlcolem  41172  cdlemg48  41183  tgrpov  41194  tendoco2  41214  tendoplco2  41225  cdlemh1  41261  cdlemi1  41264  cdlemi2  41265  cdlemj3  41269  tendoid0  41271  cdlemk1  41277  cdlemk2  41278  cdlemk4  41280  cdlemk8  41284  cdlemk9  41285  cdlemk9bN  41286  cdlemk10  41289  cdlemk26b-3  41351  cdlemk26-3  41352  cdlemk28-3  41354  cdlemk37  41360  cdlemk39  41362  cdlemkfid1N  41367  cdlemkid1  41368  cdlemky  41372  cdlemkyu  41373  cdlemk19ylem  41376  cdlemk19xlem  41388  cdlemk11t  41392  cdlemk51  41399  cdlemkyyN  41408  cdleml6  41427  cdleml7  41428  cdleml8  41429  cdleml9  41430  erngdvlem4  41437  erngdvlem4-rN  41445  tendospcanN  41469  dia11N  41494  cdlemm10N  41564  dib11N  41606  dicvaddcl  41636  dicvscacl  41637  cdlemn6  41648  dihvalcq2  41693  dihopelvalcpre  41694  dihord6b  41706  dihord5apre  41708  dihmeetlem1N  41736  dihmeetlem2N  41745  dihglbcpreN  41746  dihjatc1  41757  dihmeetlem20N  41772  dih1dimatlem0  41774  dihatlat  41780  dihglblem6  41786  dochexmidlem4  41909  mapdpglem32  42151  mapdh8ad  42225  mapdh9aOLDN  42236  hdmap11lem2  42288  hdmap14lem6  42319  frlmfzowrdb  42949  flt4lem5  43083  mzpsubst  43180  pellex  43263  pellfundex  43314  pellfund14gap  43315  qirropth  43336  rmxypos  43375  congmul  43395  congsub  43398  mzpcong  43400  coprmdvdsb  43413  jm2.15nn0  43431  jm2.16nn0  43432  rpnnen3lem  43459  idomsubgmo  43621  relexp01min  44140  mullimc  46046  islptre  46049  limccog  46050  mullimcf  46053  addlimc  46076  0ellimcdiv  46077  limsupre3lem  46160  stoweidlem57  46485  fourierdlem48  46582  fourierdlem80  46614  fourierdlem113  46647  ovncvrrp  46992  opnvonmbllem2  47061  ovolval5lem3  47082  ovnovollem3  47086  grlimedgclnbgr  48471  itsclc0lem1  49232  itsclc0lem2  49233  itschlc0yqe  49236  itscnhlc0xyqsol  49241  itschlc0xyqsol1  49242  swapffunc  49757  fucofunc  49834  fucoppc  49885