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  7803  fpr3g  8228  tfrlem5  8312  omeulem1  8510  omeulem2  8511  uniinqs  8737  elfiun  9336  tcrank  9799  isfin2-2  10232  konigthlem  10482  gruen  10726  addlid  11320  mulcan  11778  mulcan2  11779  divass  11818  divdir  11825  div11OLD  11829  muldivdir  11838  subdivcomb1  11841  subdivcomb2  11842  divcan5  11848  ltmul1  11996  ltdiv1  12011  ltmuldiv  12020  lediv2  12037  xaddass2  13193  xlt2add  13203  xmulasslem3  13229  xadddi2  13240  expaddz  14059  expmulz  14061  muldivbinom2  14216  resqrtcl  15206  o1add  15567  o1mul  15568  o1sub  15569  dvdsadd2b  16266  dvdsgcd  16504  rpexp12i  16685  pythagtriplem3  16780  pcpremul  16805  pceu  16808  pcqmul  16815  pcqdiv  16819  setsstruct  17137  f1ocpbllem  17479  funcoppc  17833  funcres  17854  catcisolem  18068  1stfcl  18154  2ndfcl  18155  prfcl  18160  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  latjlej12  18412  latmlem12  18428  latj4  18446  latj4rot  18447  symgsssg  19433  symgfisg  19434  psgnunilem4  19463  odcong  19515  cmn4  19767  ablsub4  19776  abladdsub4  19777  lsm4  19826  abvdom  20798  abvres  20799  abvtrivd  20800  orngmul  20833  lspsolvlem  21132  lbsextlem2  21149  lidlsubcl  21214  frlmbas3  21766  matmulcell  22420  marrepeval  22538  ma1repveval  22546  submaeval  22557  mdetunilem3  22589  mdetuni0  22596  mdetmul  22598  minmar1eval  22624  nllyrest  23461  hausflimlem  23954  tsmsxp  24130  psmetlecl  24290  xmetlecl  24321  prdsxmetlem  24343  ngpocelbl  24679  bndth  24935  cph2ass  25190  iscau3  25255  dvres2  25889  coemullem  26225  vieta1  26289  aalioulem4  26312  cxpcn3lem  26724  angcan  26779  dchrvmasumlema  27477  logdivsum  27510  abvcxp  27592  padicabv  27607  nosupbnd1lem4  27689  nosupbnd1lem5  27690  noinfbnd1lem4  27704  cofcut1  27926  cofcut2  27928  divmulsw  28199  precsexlem8  28220  precsexlem9  28221  bdayfinbndlem1  28473  ax5seglem3  29014  ax5seglem6  29017  axpasch  29024  axeuclid  29046  axcontlem4  29050  axcontlem8  29054  wlkl1loop  29721  trlsonwlkon  29791  pthontrlon  29830  wspthsswwlknon  30004  frgr2wwlkeqm  30416  adjlnop  32172  xreceu  32996  rhmdvd  33399  measvunilem  34372  measvunilem0  34373  measres  34382  bnj1128  35148  umgr2cycllem  35338  umgr2cycl  35339  satfv1fvfmla1  35621  cgrcomim  36187  cgrcoml  36194  cgrcomr  36195  cgrdegen  36202  segconeu  36209  btwnintr  36217  btwnexch3  36218  btwnouttr2  36220  btwnouttr  36222  btwnexch  36223  trisegint  36226  lineext  36274  linecgr  36279  lineid  36281  idinside  36282  btwnconn1lem3  36287  btwnconn1lem4  36288  btwnconn1lem7  36291  btwnconn1lem14  36298  btwnconn2  36300  midofsegid  36302  btwnoutside  36323  outsideoftr  36327  lineunray  36345  lineelsb2  36346  cnres2  38098  heibor  38156  lsmcv2  39489  lcvat  39490  lcvexchlem4  39497  lcvexchlem5  39498  lfladd  39526  lflsub  39527  lflmul  39528  lshpkrlem4  39573  latm4  39693  omlmod1i2N  39720  cvlatexch3  39798  cvlsupr7  39808  hlatj4  39834  hlrelat3  39872  cvrval3  39873  atcvrj1  39891  atlelt  39898  2atlt  39899  2atjm  39905  3noncolr2  39909  athgt  39916  3dimlem2  39919  3dimlem4  39924  3dimlem4OLDN  39925  3dim3  39929  1cvratex  39933  ps-1  39937  ps-2  39938  hlatexch3N  39940  llnle  39978  atcvrlln2  39979  atcvrlln  39980  lplni2  39997  lplnle  40000  lplnnle2at  40001  llncvrlpln2  40017  lplnexllnN  40024  2llnmeqat  40031  lvolnle3at  40042  4atlem0ae  40054  lplncvrlvol2  40075  lnjatN  40240  lncvrat  40242  cdlemblem  40253  elpaddri  40262  paddasslem2  40281  paddasslem16  40295  padd4N  40300  hlmod1i  40316  dalawlem2  40332  pclfinN  40360  pexmidlem4N  40433  pl42lem1N  40439  lhp2lt  40461  lhpexle1  40468  lhpexle2lem  40469  lhpj1  40482  lhpmcvr5N  40487  lhp2at0  40492  lhp2atnle  40493  lhp2at0nle  40495  lhple  40502  lhpat  40503  lhpat4N  40504  4atexlempnq  40515  4atexlem7  40535  4atex  40536  ltrn11  40586  ltrnle  40589  ltrnm  40591  ltrnj  40592  ltrncvr  40593  ltrnel  40599  ltrncnvel  40602  ltrncnv  40606  trlval2  40623  trlcnv  40625  trljat1  40626  trljat2  40627  trlat  40629  trl0  40630  trlnidat  40633  trlnid  40639  cdlemc1  40651  cdlemc2  40652  cdlemc5  40655  cdlemd2  40659  cdlemd7  40664  cdlemd8  40665  cdlemd9  40666  cdleme0e  40677  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme5  40700  cdleme10  40714  cdleme11a  40720  cdleme11c  40721  cdleme11h  40726  cdleme11j  40727  cdleme0nex  40750  cdleme18a  40751  cdleme18b  40752  cdleme22gb  40754  cdleme20zN  40761  cdleme20c  40771  cdleme20k  40779  cdleme21a  40785  cdleme21b  40786  cdleme21c  40787  cdleme21h  40794  cdleme22b  40801  cdleme22d  40803  cdleme22f  40806  cdleme25a  40813  cdleme25c  40815  cdleme25dN  40816  cdleme26ee  40820  cdleme30a  40838  cdlemefr29bpre0N  40866  cdlemefr29clN  40867  cdlemefr32fvaN  40869  cdlemefr32fva1  40870  cdlemefs29bpre0N  40876  cdlemefs29bpre1N  40877  cdlemefs29cpre1N  40878  cdlemefs29clN  40879  cdleme43fsv1snlem  40880  cdlemefs32fvaN  40882  cdlemefs32fva1  40883  cdlemefs31fv1  40884  cdleme36a  40920  cdleme39a  40925  cdleme42a  40931  cdleme42c  40932  cdleme17d3  40956  cdleme48fv  40959  cdleme48bw  40962  cdleme48b  40963  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemeg46gfv  40990  cdleme48d  40995  cdleme50trn2a  41010  cdleme50trn2  41011  cdleme50ltrn  41017  cdlemf1  41021  cdlemf  41023  trlord  41029  cdlemg2dN  41050  cdlemg2fvlem  41054  cdlemg2l  41063  cdlemg7fvbwN  41067  cdlemg7aN  41085  cdlemg10bALTN  41096  cdlemg10c  41099  cdlemg17a  41121  cdlemg17dALTN  41124  cdlemg31b0a  41155  cdlemg31a  41157  cdlemg31b  41158  cdlemg34  41172  cdlemg36  41174  ltrnco  41179  trlcoabs2N  41182  trlcolem  41186  cdlemg48  41197  tgrpov  41208  tendoco2  41228  tendoplco2  41239  cdlemh1  41275  cdlemi1  41278  cdlemi2  41279  cdlemj3  41283  tendoid0  41285  cdlemk1  41291  cdlemk2  41292  cdlemk4  41294  cdlemk8  41298  cdlemk9  41299  cdlemk9bN  41300  cdlemk10  41303  cdlemk26b-3  41365  cdlemk26-3  41366  cdlemk28-3  41368  cdlemk37  41374  cdlemk39  41376  cdlemkfid1N  41381  cdlemkid1  41382  cdlemky  41386  cdlemkyu  41387  cdlemk19ylem  41390  cdlemk19xlem  41402  cdlemk11t  41406  cdlemk51  41413  cdlemkyyN  41422  cdleml6  41441  cdleml7  41442  cdleml8  41443  cdleml9  41444  erngdvlem4  41451  erngdvlem4-rN  41459  tendospcanN  41483  dia11N  41508  cdlemm10N  41578  dib11N  41620  dicvaddcl  41650  dicvscacl  41651  cdlemn6  41662  dihvalcq2  41707  dihopelvalcpre  41708  dihord6b  41720  dihord5apre  41722  dihmeetlem1N  41750  dihmeetlem2N  41759  dihglbcpreN  41760  dihjatc1  41771  dihmeetlem20N  41786  dih1dimatlem0  41788  dihatlat  41794  dihglblem6  41800  dochexmidlem4  41923  mapdpglem32  42165  mapdh8ad  42239  mapdh9aOLDN  42250  hdmap11lem2  42302  hdmap14lem6  42333  frlmfzowrdb  42963  flt4lem5  43097  mzpsubst  43194  pellex  43281  pellfundex  43332  pellfund14gap  43333  qirropth  43354  rmxypos  43393  congmul  43413  congsub  43416  mzpcong  43418  coprmdvdsb  43431  jm2.15nn0  43449  jm2.16nn0  43450  rpnnen3lem  43477  idomsubgmo  43639  relexp01min  44158  mullimc  46064  islptre  46067  limccog  46068  mullimcf  46071  addlimc  46094  0ellimcdiv  46095  limsupre3lem  46178  stoweidlem57  46503  fourierdlem48  46600  fourierdlem80  46632  fourierdlem113  46665  ovncvrrp  47010  opnvonmbllem2  47079  ovolval5lem3  47100  ovnovollem3  47104  grlimedgclnbgr  48483  itsclc0lem1  49244  itsclc0lem2  49245  itschlc0yqe  49248  itscnhlc0xyqsol  49253  itschlc0xyqsol1  49254  swapffunc  49769  fucofunc  49846  fucoppc  49897