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  7811  fpr3g  8237  tfrlem5  8321  omeulem1  8519  omeulem2  8520  uniinqs  8746  elfiun  9345  tcrank  9808  isfin2-2  10241  konigthlem  10491  gruen  10735  addlid  11328  mulcan  11786  mulcan2  11787  divass  11826  divdir  11833  div11OLD  11837  muldivdir  11846  subdivcomb1  11848  subdivcomb2  11849  divcan5  11855  ltmul1  12003  ltdiv1  12018  ltmuldiv  12027  lediv2  12044  xaddass2  13177  xlt2add  13187  xmulasslem3  13213  xadddi2  13224  expaddz  14041  expmulz  14043  muldivbinom2  14198  resqrtcl  15188  o1add  15549  o1mul  15550  o1sub  15551  dvdsadd2b  16245  dvdsgcd  16483  rpexp12i  16663  pythagtriplem3  16758  pcpremul  16783  pceu  16786  pcqmul  16793  pcqdiv  16797  setsstruct  17115  f1ocpbllem  17457  funcoppc  17811  funcres  17832  catcisolem  18046  1stfcl  18132  2ndfcl  18133  prfcl  18138  evlfcl  18157  curf1cl  18163  curfcl  18167  hofcl  18194  latjlej12  18390  latmlem12  18406  latj4  18424  latj4rot  18425  symgsssg  19408  symgfisg  19409  psgnunilem4  19438  odcong  19490  cmn4  19742  ablsub4  19751  abladdsub4  19752  lsm4  19801  abvdom  20775  abvres  20776  abvtrivd  20777  orngmul  20810  lspsolvlem  21109  lbsextlem2  21126  lidlsubcl  21191  frlmbas3  21743  matmulcell  22401  marrepeval  22519  ma1repveval  22527  submaeval  22538  mdetunilem3  22570  mdetuni0  22577  mdetmul  22579  minmar1eval  22605  nllyrest  23442  hausflimlem  23935  tsmsxp  24111  psmetlecl  24271  xmetlecl  24302  prdsxmetlem  24324  ngpocelbl  24660  bndth  24925  cph2ass  25181  iscau3  25246  dvres2  25881  coemullem  26223  vieta1  26288  aalioulem4  26311  cxpcn3lem  26725  angcan  26780  dchrvmasumlema  27479  logdivsum  27512  abvcxp  27594  padicabv  27609  nosupbnd1lem4  27691  nosupbnd1lem5  27692  noinfbnd1lem4  27706  cofcut1  27928  cofcut2  27930  divmulsw  28201  precsexlem8  28222  precsexlem9  28223  bdayfinbndlem1  28475  ax5seglem3  29016  ax5seglem6  29019  axpasch  29026  axeuclid  29048  axcontlem4  29052  axcontlem8  29056  wlkl1loop  29723  trlsonwlkon  29793  pthontrlon  29832  wspthsswwlknon  30006  frgr2wwlkeqm  30418  adjlnop  32173  xreceu  33013  rhmdvd  33416  measvunilem  34389  measvunilem0  34390  measres  34399  bnj1128  35165  umgr2cycllem  35353  umgr2cycl  35354  satfv1fvfmla1  35636  cgrcomim  36202  cgrcoml  36209  cgrcomr  36210  cgrdegen  36217  segconeu  36224  btwnintr  36232  btwnexch3  36233  btwnouttr2  36235  btwnouttr  36237  btwnexch  36238  trisegint  36241  lineext  36289  linecgr  36294  lineid  36296  idinside  36297  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem7  36306  btwnconn1lem14  36313  btwnconn2  36315  midofsegid  36317  btwnoutside  36338  outsideoftr  36342  lineunray  36360  lineelsb2  36361  cnres2  38008  heibor  38066  lsmcv2  39399  lcvat  39400  lcvexchlem4  39407  lcvexchlem5  39408  lfladd  39436  lflsub  39437  lflmul  39438  lshpkrlem4  39483  latm4  39603  omlmod1i2N  39630  cvlatexch3  39708  cvlsupr7  39718  hlatj4  39744  hlrelat3  39782  cvrval3  39783  atcvrj1  39801  atlelt  39808  2atlt  39809  2atjm  39815  3noncolr2  39819  athgt  39826  3dimlem2  39829  3dimlem4  39834  3dimlem4OLDN  39835  3dim3  39839  1cvratex  39843  ps-1  39847  ps-2  39848  hlatexch3N  39850  llnle  39888  atcvrlln2  39889  atcvrlln  39890  lplni2  39907  lplnle  39910  lplnnle2at  39911  llncvrlpln2  39927  lplnexllnN  39934  2llnmeqat  39941  lvolnle3at  39952  4atlem0ae  39964  lplncvrlvol2  39985  lnjatN  40150  lncvrat  40152  cdlemblem  40163  elpaddri  40172  paddasslem2  40191  paddasslem16  40205  padd4N  40210  hlmod1i  40226  dalawlem2  40242  pclfinN  40270  pexmidlem4N  40343  pl42lem1N  40349  lhp2lt  40371  lhpexle1  40378  lhpexle2lem  40379  lhpj1  40392  lhpmcvr5N  40397  lhp2at0  40402  lhp2atnle  40403  lhp2at0nle  40405  lhple  40412  lhpat  40413  lhpat4N  40414  4atexlempnq  40425  4atexlem7  40445  4atex  40446  ltrn11  40496  ltrnle  40499  ltrnm  40501  ltrnj  40502  ltrncvr  40503  ltrnel  40509  ltrncnvel  40512  ltrncnv  40516  trlval2  40533  trlcnv  40535  trljat1  40536  trljat2  40537  trlat  40539  trl0  40540  trlnidat  40543  trlnid  40549  cdlemc1  40561  cdlemc2  40562  cdlemc5  40565  cdlemd2  40569  cdlemd7  40574  cdlemd8  40575  cdlemd9  40576  cdleme0e  40587  cdleme3g  40604  cdleme3h  40605  cdleme3  40607  cdleme5  40610  cdleme10  40624  cdleme11a  40630  cdleme11c  40631  cdleme11h  40636  cdleme11j  40637  cdleme0nex  40660  cdleme18a  40661  cdleme18b  40662  cdleme22gb  40664  cdleme20zN  40671  cdleme20c  40681  cdleme20k  40689  cdleme21a  40695  cdleme21b  40696  cdleme21c  40697  cdleme21h  40704  cdleme22b  40711  cdleme22d  40713  cdleme22f  40716  cdleme25a  40723  cdleme25c  40725  cdleme25dN  40726  cdleme26ee  40730  cdleme30a  40748  cdlemefr29bpre0N  40776  cdlemefr29clN  40777  cdlemefr32fvaN  40779  cdlemefr32fva1  40780  cdlemefs29bpre0N  40786  cdlemefs29bpre1N  40787  cdlemefs29cpre1N  40788  cdlemefs29clN  40789  cdleme43fsv1snlem  40790  cdlemefs32fvaN  40792  cdlemefs32fva1  40793  cdlemefs31fv1  40794  cdleme36a  40830  cdleme39a  40835  cdleme42a  40841  cdleme42c  40842  cdleme17d3  40866  cdleme48fv  40869  cdleme48bw  40872  cdleme48b  40873  cdlemeg46rgv  40898  cdlemeg46req  40899  cdlemeg46gfv  40900  cdleme48d  40905  cdleme50trn2a  40920  cdleme50trn2  40921  cdleme50ltrn  40927  cdlemf1  40931  cdlemf  40933  trlord  40939  cdlemg2dN  40960  cdlemg2fvlem  40964  cdlemg2l  40973  cdlemg7fvbwN  40977  cdlemg7aN  40995  cdlemg10bALTN  41006  cdlemg10c  41009  cdlemg17a  41031  cdlemg17dALTN  41034  cdlemg31b0a  41065  cdlemg31a  41067  cdlemg31b  41068  cdlemg34  41082  cdlemg36  41084  ltrnco  41089  trlcoabs2N  41092  trlcolem  41096  cdlemg48  41107  tgrpov  41118  tendoco2  41138  tendoplco2  41149  cdlemh1  41185  cdlemi1  41188  cdlemi2  41189  cdlemj3  41193  tendoid0  41195  cdlemk1  41201  cdlemk2  41202  cdlemk4  41204  cdlemk8  41208  cdlemk9  41209  cdlemk9bN  41210  cdlemk10  41213  cdlemk26b-3  41275  cdlemk26-3  41276  cdlemk28-3  41278  cdlemk37  41284  cdlemk39  41286  cdlemkfid1N  41291  cdlemkid1  41292  cdlemky  41296  cdlemkyu  41297  cdlemk19ylem  41300  cdlemk19xlem  41312  cdlemk11t  41316  cdlemk51  41323  cdlemkyyN  41332  cdleml6  41351  cdleml7  41352  cdleml8  41353  cdleml9  41354  erngdvlem4  41361  erngdvlem4-rN  41369  tendospcanN  41393  dia11N  41418  cdlemm10N  41488  dib11N  41530  dicvaddcl  41560  dicvscacl  41561  cdlemn6  41572  dihvalcq2  41617  dihopelvalcpre  41618  dihord6b  41630  dihord5apre  41632  dihmeetlem1N  41660  dihmeetlem2N  41669  dihglbcpreN  41670  dihjatc1  41681  dihmeetlem20N  41696  dih1dimatlem0  41698  dihatlat  41704  dihglblem6  41710  dochexmidlem4  41833  mapdpglem32  42075  mapdh8ad  42149  mapdh9aOLDN  42160  hdmap11lem2  42212  hdmap14lem6  42243  frlmfzowrdb  42868  flt4lem5  43002  mzpsubst  43099  pellex  43186  pellfundex  43237  pellfund14gap  43238  qirropth  43259  rmxypos  43298  congmul  43318  congsub  43321  mzpcong  43323  coprmdvdsb  43336  jm2.15nn0  43354  jm2.16nn0  43355  rpnnen3lem  43382  idomsubgmo  43544  relexp01min  44063  mullimc  45970  islptre  45973  limccog  45974  mullimcf  45977  addlimc  46000  0ellimcdiv  46001  limsupre3lem  46084  stoweidlem57  46409  fourierdlem48  46506  fourierdlem80  46538  fourierdlem113  46571  ovncvrrp  46916  opnvonmbllem2  46985  ovolval5lem3  47006  ovnovollem3  47010  grlimedgclnbgr  48349  itsclc0lem1  49110  itsclc0lem2  49111  itschlc0yqe  49114  itscnhlc0xyqsol  49119  itschlc0xyqsol1  49120  swapffunc  49635  fucofunc  49712  fucoppc  49763