Theorem simp3r 1252

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp3r	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Proof of Theorem simp3r

Step	Hyp	Ref	Expression
1		simpr 473	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant3 1158	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  simpl3rOLD  1297  simpr3rOLD  1309  simp13r  1381  simp23r  1387  simp33r  1393  f1oiso2  6822  tfisi  7284  tfrlem5  7708  omeulem1  7895  omeulem2  7896  elfiun  8571  isfin2-2  9422  addid2  10500  mulcan  10945  mulcan2  10946  divass  10984  divdir  10991  div11  10994  ltdiv1  11168  ltmuldiv  11177  lediv2  11194  xaddass2  12294  xlt2add  12304  expaddz  13123  expmulz  13125  resqrex  14210  resqrtcl  14213  o1add  14563  o1mul  14564  o1sub  14565  dvdsgcd  15476  rpexp12i  15647  pythagtriplem4  15737  pythagtriplem11  15743  pythagtriplem13  15745  pcpremul  15761  pceu  15764  pcqmul  15771  pcqdiv  15775  f1ocpbllem  16385  funcoppc  16735  funcres  16756  catcisolem  16956  1stfcl  17038  2ndfcl  17039  prfcl  17044  evlfcl  17063  curf1cl  17069  curfcl  17073  hofcl  17100  latjlej12  17268  latmlem12  17284  latj4  17302  latj4rot  17303  symgsssg  18084  symgfisg  18085  odcong  18165  cmn4  18409  ablsub4  18415  abladdsub4  18416  lsm4  18460  abvdom  19038  abvtrivd  19040  lspsolvlem  19346  lbsextlem2  19364  lidlsubcl  19421  frlmbas3  20321  matinvgcell  20447  matmulcell  20457  matmulcellOLD  20458  ma1repveval  20584  mdetunilem3  20627  mdetuni0  20634  mdetmul  20636  hausflimlem  21992  psmetlecl  22329  xmetlecl  22360  prdsxmetlem  22382  xblcntrps  22424  xblcntr  22425  bndth  22966  cph2ass  23221  iscau3  23284  dvres2  23886  coemullem  24216  vieta1  24277  aalioulem4  24300  cxpcn3lem  24698  angcan  24742  divsqrtsumlem  24916  dchrmusumlema  25392  dchrvmasumlema  25399  dchrisum0lema  25413  logdivsum  25432  padicabv  25529  ax5seglem3  26021  ax5seglem6  26024  axpasch  26031  axeuclid  26053  axcontlem4  26057  axcontlem8  26061  trlsonistrl  26829  pthonispth  26866  spthonisspth  26870  wspthneq1eq2  26983  frgr2wwlkeqm  27502  adjlnop  29269  xreceu  29951  orngmul  30124  rhmdvd  30142  measvunilem  30596  measvuni  30598  bnj1128  31376  cgrcomim  32412  cgrcoml  32419  cgrcomr  32420  cgrdegen  32427  segconeu  32434  btwnintr  32442  btwnexch3  32443  btwnouttr2  32445  btwnouttr  32447  btwnexch  32448  ifscgr  32467  lineext  32499  linecgr  32504  lineid  32506  idinside  32507  btwnconn1lem3  32512  btwnconn1lem4  32513  btwnconn1lem14  32523  btwnconn2  32525  btwnconn3  32526  midofsegid  32527  btwnoutside  32548  outsideoftr  32552  lineunray  32570  lineelsb2  32571  itg2addnclem  33768  cnres2  33868  heibor  33926  lsmcv2  34804  lcvat  34805  lcvexchlem4  34812  lcvexchlem5  34813  lfladd  34841  lflsub  34842  lflmul  34843  lshpkrlem4  34888  latm4  35008  omlmod1i2N  35035  cvlsupr7  35123  cvlsupr8  35124  hlatj4  35149  hlrelat3  35187  cvrval3  35188  atcvrj1  35206  atlelt  35213  2atlt  35214  2atjm  35220  3noncolr2  35224  athgt  35231  3dimlem2  35234  3dimlem4OLDN  35240  1cvratex  35248  ps-1  35252  ps-2  35253  hlatexch3N  35255  llnle  35293  atcvrlln2  35294  atcvrlln  35295  lplni2  35312  lplnle  35315  lplnnle2at  35316  lplnnlelln  35318  llncvrlpln2  35332  2llnmeqat  35346  lvolnle3at  35357  lvolnlelln  35359  4atlem0ae  35369  lneq2at  35553  lnjatN  35555  lncvrat  35557  2lnat  35559  elpaddri  35577  paddasslem2  35596  padd4N  35615  hlmod1i  35631  llnexchb2  35644  dalawlem2  35647  pclfinN  35675  pexmidlem4N  35748  pl42lem1N  35754  lhp2lt  35776  lhpexle1  35783  lhpexle2lem  35784  lhpj1  35797  lhpmcvr5N  35802  lhp2at0  35807  lhp2at0nle  35810  lhple  35817  lhpat  35818  lhpat4N  35819  4atexlemnslpq  35831  4atexlem7  35850  ltrn11  35901  ltrnle  35904  ltrnm  35906  ltrnj  35907  ltrncvr  35908  ltrnel  35914  ltrncnvel  35917  ltrncnv  35921  trlat  35944  trl0  35945  trlnidat  35948  trlnid  35954  ltrnatlw  35958  trlne  35960  trlval4  35963  cdlemc5  35970  cdlemd2  35974  cdlemd7  35979  cdlemd8  35980  cdlemd9  35981  cdleme0c  35988  cdleme0e  35992  cdleme0fN  35993  cdleme3g  36009  cdleme3h  36010  cdleme5  36015  cdleme11c  36036  cdleme11h  36041  cdleme11j  36042  cdleme11k  36043  cdleme0nex  36065  cdleme18a  36066  cdleme22gb  36069  cdleme20zN  36076  cdleme20c  36086  cdleme20k  36094  cdleme21a  36100  cdleme21b  36101  cdleme21c  36102  cdleme21ct  36104  cdleme21h  36109  cdleme22d  36118  cdleme22f  36121  cdleme26ee  36135  cdleme30a  36153  cdlemefs45eN  36206  cdleme36a  36235  cdleme36m  36236  cdleme39a  36240  cdleme42b  36253  cdleme43dN  36267  cdlemeg47rv2  36285  cdlemeg46sfg  36295  cdlemeg46rjgN  36297  cdlemeg46rgv  36303  cdlemeg46req  36304  cdlemeg46gfv  36305  cdleme48d  36310  cdleme50ltrn  36332  cdlemf1  36336  cdlemf  36338  cdlemg2dN  36365  cdlemg2fvlem  36369  cdlemg2l  36378  cdlemg7fvbwN  36382  cdlemg7aN  36400  cdlemg10c  36414  cdlemg17a  36436  cdlemg17dALTN  36439  cdlemg18a  36453  cdlemg18b  36454  cdlemg31b0a  36470  cdlemg31a  36472  cdlemg31b  36473  ltrnco  36494  cdlemg48  36512  tgrpov  36523  tendoco2  36543  tendoplco2  36554  cdlemh1  36590  cdlemk1  36606  cdlemk26b-3  36680  cdlemk27-3  36682  cdlemk28-3  36683  cdlemk34  36685  cdlemkfid1N  36696  cdlemkid3N  36708  cdlemkid4  36709  cdlemk35s-id  36713  cdlemk39s-id  36715  cdlemk51  36728  tendospcanN  36798  cdlemm10N  36893  dicvaddcl  36965  dicvscacl  36966  cdlemn6  36977  dihvalcq2  37022  dihord6b  37035  dihord5apre  37037  dihglbcpreN  37075  dihjatc1  37086  dihmeetlem20N  37101  dih1dimatlem0  37103  dihglblem6  37115  dochexmidlem4  37238  mapdpglem32  37480  mapdh8ad  37554  mapdh9aOLDN  37565  hdmap11lem2  37617  hdmap14lem6  37648  mzpmfp  37806  mzpsubst  37807  pellex  37895  pellfundex  37946  pellfund14gap  37947  qirropth  37968  rmxypos  38009  congmul  38029  congsub  38032  mzpcong  38034  coprmdvdsb  38047  jm2.15nn0  38065  jm2.16nn0  38066  rpnnen3lem  38093  idomsubgmo  38271  relexp01min  38499  mullimc  40322  islptre  40325  mullimcf  40329  addlimc  40354  0ellimcdiv  40355  limsupre3lem  40438  limsupre3uzlem  40441  fourierdlem48  40844  fourierdlem80  40876  opnvonmbllem2  41323  ovolval5lem3  41344  ovnovollem3  41348  lincfsuppcl  42764  lindslinindimp2lem3  42811