Theorem simp3r 1204

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 484	. 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:  simp13r  1291  simp23r  1297  simp33r  1303  f1oiso2  7300  tfisi  7803  tfrlem5  8312  omeulem1  8510  omeulem2  8511  elfiun  9336  isfin2-2  10232  addlid  11320  mulcan  11778  mulcan2  11779  divass  11818  divdir  11825  div11OLD  11829  ltdiv1  12011  ltmuldiv  12020  lediv2  12037  xaddass2  13193  xlt2add  13203  expaddz  14059  expmulz  14061  resqrex  15203  resqrtcl  15206  o1add  15567  o1mul  15568  o1sub  15569  dvdsgcd  16504  rpexp12i  16685  pythagtriplem4  16781  pythagtriplem11  16787  pythagtriplem13  16789  pcpremul  16805  pceu  16808  pcqmul  16815  pcqdiv  16819  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  odcong  19515  cmn4  19767  ablsub4  19776  abladdsub4  19777  lsm4  19826  abvdom  20798  abvtrivd  20800  orngmul  20833  lspsolvlem  21132  lbsextlem2  21149  lidlsubcl  21214  frlmbas3  21766  matinvgcell  22410  matmulcell  22420  ma1repveval  22546  mdetunilem3  22589  mdetuni0  22596  mdetmul  22598  hausflimlem  23954  psmetlecl  24290  xmetlecl  24321  prdsxmetlem  24343  xblcntrps  24385  xblcntr  24386  bndth  24935  cph2ass  25190  iscau3  25255  dvres2  25889  coemullem  26225  vieta1  26289  aalioulem4  26312  cxpcn3lem  26724  angcan  26779  divsqrtsumlem  26957  dchrmusumlema  27470  dchrvmasumlema  27477  dchrisum0lema  27491  logdivsum  27510  padicabv  27607  cofcut1  27926  cofcut2  27928  divmulsw  28199  precsexlem8  28220  precsexlem9  28221  bdayfinbndlem1  28473  ax5seglem3  29014  ax5seglem6  29017  axpasch  29024  axeuclid  29046  axcontlem4  29050  axcontlem8  29054  trlsonistrl  29790  pthonispth  29829  spthonisspth  29833  wspthneq1eq2  29943  frgr2wwlkeqm  30416  adjlnop  32172  xreceu  32996  rhmdvd  33399  measvunilem  34372  measvuni  34374  bnj1128  35148  umgr2cycl  35339  satfv1fvfmla1  35621  cgrcomim  36187  cgrcoml  36194  cgrcomr  36195  cgrdegen  36202  segconeu  36209  btwnintr  36217  btwnexch3  36218  btwnouttr2  36220  btwnouttr  36222  btwnexch  36223  ifscgr  36242  lineext  36274  linecgr  36279  lineid  36281  idinside  36282  btwnconn1lem3  36287  btwnconn1lem4  36288  btwnconn1lem14  36298  btwnconn2  36300  btwnconn3  36301  midofsegid  36302  btwnoutside  36323  outsideoftr  36327  lineunray  36345  lineelsb2  36346  itg2addnclem  38006  cnres2  38098  heibor  38156  lsmcv2  39489  lcvat  39490  lcvexchlem4  39497  lcvexchlem5  39498  lfladd  39526  lflsub  39527  lflmul  39528  lshpkrlem4  39573  latm4  39693  omlmod1i2N  39720  cvlsupr7  39808  cvlsupr8  39809  hlatj4  39834  hlrelat3  39872  cvrval3  39873  atcvrj1  39891  atlelt  39898  2atlt  39899  2atjm  39905  3noncolr2  39909  athgt  39916  3dimlem2  39919  3dimlem4OLDN  39925  1cvratex  39933  ps-1  39937  ps-2  39938  hlatexch3N  39940  llnle  39978  atcvrlln2  39979  atcvrlln  39980  lplni2  39997  lplnle  40000  lplnnle2at  40001  lplnnlelln  40003  llncvrlpln2  40017  2llnmeqat  40031  lvolnle3at  40042  lvolnlelln  40044  4atlem0ae  40054  lneq2at  40238  lnjatN  40240  lncvrat  40242  2lnat  40244  elpaddri  40262  paddasslem2  40281  padd4N  40300  hlmod1i  40316  llnexchb2  40329  dalawlem2  40332  pclfinN  40360  pexmidlem4N  40433  pl42lem1N  40439  lhp2lt  40461  lhpexle1  40468  lhpexle2lem  40469  lhpj1  40482  lhpmcvr5N  40487  lhp2at0  40492  lhp2at0nle  40495  lhple  40502  lhpat  40503  lhpat4N  40504  4atexlemnslpq  40516  4atexlem7  40535  ltrn11  40586  ltrnle  40589  ltrnm  40591  ltrnj  40592  ltrncvr  40593  ltrnel  40599  ltrncnvel  40602  ltrncnv  40606  trlat  40629  trl0  40630  trlnidat  40633  trlnid  40639  ltrnatlw  40643  trlne  40645  trlval4  40648  cdlemc5  40655  cdlemd2  40659  cdlemd7  40664  cdlemd8  40665  cdlemd9  40666  cdleme0c  40673  cdleme0e  40677  cdleme0fN  40678  cdleme3g  40694  cdleme3h  40695  cdleme5  40700  cdleme11c  40721  cdleme11h  40726  cdleme11j  40727  cdleme11k  40728  cdleme0nex  40750  cdleme18a  40751  cdleme22gb  40754  cdleme20zN  40761  cdleme20c  40771  cdleme20k  40779  cdleme21a  40785  cdleme21b  40786  cdleme21c  40787  cdleme21ct  40789  cdleme21h  40794  cdleme22d  40803  cdleme22f  40806  cdleme26ee  40820  cdleme30a  40838  cdlemefs45eN  40891  cdleme36a  40920  cdleme36m  40921  cdleme39a  40925  cdleme42b  40938  cdleme43dN  40952  cdlemeg47rv2  40970  cdlemeg46sfg  40980  cdlemeg46rjgN  40982  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemeg46gfv  40990  cdleme48d  40995  cdleme50ltrn  41017  cdlemf1  41021  cdlemf  41023  cdlemg2dN  41050  cdlemg2fvlem  41054  cdlemg2l  41063  cdlemg7fvbwN  41067  cdlemg7aN  41085  cdlemg10c  41099  cdlemg17a  41121  cdlemg17dALTN  41124  cdlemg18a  41138  cdlemg18b  41139  cdlemg31b0a  41155  cdlemg31a  41157  cdlemg31b  41158  ltrnco  41179  cdlemg48  41197  tgrpov  41208  tendoco2  41228  tendoplco2  41239  cdlemh1  41275  cdlemk1  41291  cdlemk26b-3  41365  cdlemk27-3  41367  cdlemk28-3  41368  cdlemk34  41370  cdlemkfid1N  41381  cdlemkid3N  41393  cdlemkid4  41394  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk51  41413  tendospcanN  41483  cdlemm10N  41578  dicvaddcl  41650  dicvscacl  41651  cdlemn6  41662  dihvalcq2  41707  dihord6b  41720  dihord5apre  41722  dihglbcpreN  41760  dihjatc1  41771  dihmeetlem20N  41786  dih1dimatlem0  41788  dihglblem6  41800  dochexmidlem4  41923  mapdpglem32  42165  mapdh8ad  42239  mapdh9aOLDN  42250  hdmap11lem2  42302  hdmap14lem6  42333  frlmfzowrdb  42963  mzpmfp  43193  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  mullimcf  46071  addlimc  46094  0ellimcdiv  46095  limsupre3lem  46178  limsupre3uzlem  46181  fourierdlem48  46600  fourierdlem80  46632  opnvonmbllem2  47079  ovolval5lem3  47100  ovnovollem3  47104  difltmodne  47808  isubgr3stgrlem1  48454  grlimedgclnbgr  48483  mapprop  48834  lincfsuppcl  48901  lindslinindimp2lem3  48948  itsclc0lem1  49244  itsclc0lem2  49245  itschlc0yqe  49248  itsclc0xyqsolr  49257  swapffunc  49769  fucofunc  49846  fucoppc  49897