Theorem simp3r 1221

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 490	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant3 1153	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp13r  1308  simp23r  1314  simp33r  1320  f1oiso2  7352  tfisi  7859  tfrlem5  8371  omeulem1  8574  omeulem2  8575  elfiun  9406  isfin2-2  10378  addlid  11474  mulcan  11934  mulcan2  11935  divass  11973  divdir  11980  ltdiv1  12162  ltmuldiv  12171  lediv2  12188  xaddass2  13361  xlt2add  13371  expaddz  14229  expmulz  14231  resqrex  15397  resqrtcl  15400  o1add  15761  o1mul  15762  o1sub  15763  dvdsgcd  16697  rpexp12i  16880  pythagtriplem4  16977  pythagtriplem11  16983  pythagtriplem13  16985  pcpremul  17001  pceu  17004  pcqmul  17011  pcqdiv  17015  f1ocpbllem  17676  funcoppc  18030  funcres  18051  catcisolem  18265  1stfcl  18351  2ndfcl  18352  prfcl  18357  evlfcl  18376  curf1cl  18382  curfcl  18386  hofcl  18413  latjlej12  18609  latmlem12  18625  latj4  18643  latj4rot  18644  symgsssg  19661  symgfisg  19662  odcong  19743  cmn4  19995  ablsub4  20004  abladdsub4  20005  lsm4  20054  abvdom  21067  abvtrivd  21069  orngmul  21102  lspsolvlem  21400  lbsextlem2  21417  lidlsubcl  21483  frlmbas3  22062  matinvgcell  22730  matmulcell  22740  ma1repveval  22866  mdetunilem3  22909  mdetuni0  22916  mdetmul  22918  hausflimlem  24278  psmetlecl  24614  xmetlecl  24645  prdsxmetlem  24667  xblcntrps  24709  xblcntr  24710  bndth  25259  cph2ass  25514  iscau3  25579  dvres2  26212  coemullem  26549  vieta1  26617  aalioulem4  26644  cxpcn3lem  27057  angcan  27112  divsqrtsumlem  27289  dchrmusumlema  27802  dchrvmasumlema  27809  dchrisum0lema  27823  logdivsum  27842  padicabv  27939  cofcut1  28288  cofcut2  28290  divmulsw  28561  precsexlem8  28582  precsexlem9  28583  bdayfinbndlem1  28835  ax5seglem3  29491  ax5seglem6  29494  axpasch  29501  axeuclid  29523  axcontlem4  29527  axcontlem8  29531  trlsonistrl  30273  pthonispth  30314  spthonisspth  30318  wspthneq1eq2  30431  umgr2cycllem  30728  umgr2cycl  30729  frgr2wwlkeqm  30914  adjlnop  32670  xreceu  33470  rhmdvd  33867  measvunilem  34827  measvuni  34829  bnj1128  35603  satfv1fvfmla1  36157  cgrcomim  36724  cgrcoml  36731  cgrcomr  36732  cgrdegen  36739  segconeu  36746  btwnintr  36754  btwnexch3  36755  btwnouttr2  36757  btwnouttr  36759  btwnexch  36760  ifscgr  36779  lineext  36811  linecgr  36816  lineid  36818  idinside  36819  btwnconn1lem3  36824  btwnconn1lem4  36825  btwnconn1lem14  36835  btwnconn2  36837  btwnconn3  36838  midofsegid  36839  btwnoutside  36860  outsideoftr  36864  lineunray  36882  lineelsb2  36883  itg2addnclem  38557  cnres2  38665  heibor  38723  lsmcv2  40054  lcvat  40055  lcvexchlem4  40062  lcvexchlem5  40063  lfladd  40091  lflsub  40092  lflmul  40093  lshpkrlem4  40138  latm4  40258  omlmod1i2N  40285  cvlsupr7  40373  cvlsupr8  40374  hlatj4  40399  hlrelat3  40437  cvrval3  40438  atcvrj1  40456  atlelt  40463  2atlt  40464  2atjm  40470  3noncolr2  40474  athgt  40481  3dimlem2  40484  3dimlem4OLDN  40490  1cvratex  40498  ps-1  40502  ps-2  40503  hlatexch3N  40505  llnle  40543  atcvrlln2  40544  atcvrlln  40545  lplni2  40562  lplnle  40565  lplnnle2at  40566  lplnnlelln  40568  llncvrlpln2  40582  2llnmeqat  40596  lvolnle3at  40607  lvolnlelln  40609  4atlem0ae  40619  lneq2at  40803  lnjatN  40805  lncvrat  40807  2lnat  40809  elpaddri  40827  paddasslem2  40846  padd4N  40865  hlmod1i  40881  llnexchb2  40894  dalawlem2  40897  pclfinN  40925  pexmidlem4N  40998  pl42lem1N  41004  lhp2lt  41026  lhpexle1  41033  lhpexle2lem  41034  lhpj1  41047  lhpmcvr5N  41052  lhp2at0  41057  lhp2at0nle  41060  lhple  41067  lhpat  41068  lhpat4N  41069  4atexlemnslpq  41081  4atexlem7  41100  ltrn11  41151  ltrnle  41154  ltrnm  41156  ltrnj  41157  ltrncvr  41158  ltrnel  41164  ltrncnvel  41167  ltrncnv  41171  trlat  41194  trl0  41195  trlnidat  41198  trlnid  41204  ltrnatlw  41208  trlne  41210  trlval4  41213  cdlemc5  41220  cdlemd2  41224  cdlemd7  41229  cdlemd8  41230  cdlemd9  41231  cdleme0c  41238  cdleme0e  41242  cdleme0fN  41243  cdleme3g  41259  cdleme3h  41260  cdleme5  41265  cdleme11c  41286  cdleme11h  41291  cdleme11j  41292  cdleme11k  41293  cdleme0nex  41315  cdleme18a  41316  cdleme22gb  41319  cdleme20zN  41326  cdleme20c  41336  cdleme20k  41344  cdleme21a  41350  cdleme21b  41351  cdleme21c  41352  cdleme21ct  41354  cdleme21h  41359  cdleme22d  41368  cdleme22f  41371  cdleme26ee  41385  cdleme30a  41403  cdlemefs45eN  41456  cdleme36a  41485  cdleme36m  41486  cdleme39a  41490  cdleme42b  41503  cdleme43dN  41517  cdlemeg47rv2  41535  cdlemeg46sfg  41545  cdlemeg46rjgN  41547  cdlemeg46rgv  41553  cdlemeg46req  41554  cdlemeg46gfv  41555  cdleme48d  41560  cdleme50ltrn  41582  cdlemf1  41586  cdlemf  41588  cdlemg2dN  41615  cdlemg2fvlem  41619  cdlemg2l  41628  cdlemg7fvbwN  41632  cdlemg7aN  41650  cdlemg10c  41664  cdlemg17a  41686  cdlemg17dALTN  41689  cdlemg18a  41703  cdlemg18b  41704  cdlemg31b0a  41720  cdlemg31a  41722  cdlemg31b  41723  ltrnco  41744  cdlemg48  41762  tgrpov  41773  tendoco2  41793  tendoplco2  41804  cdlemh1  41840  cdlemk1  41856  cdlemk26b-3  41930  cdlemk27-3  41932  cdlemk28-3  41933  cdlemk34  41935  cdlemkfid1N  41946  cdlemkid3N  41958  cdlemkid4  41959  cdlemk35s-id  41963  cdlemk39s-id  41965  cdlemk51  41978  tendospcanN  42048  cdlemm10N  42143  dicvaddcl  42215  dicvscacl  42216  cdlemn6  42227  dihvalcq2  42272  dihord6b  42285  dihord5apre  42287  dihglbcpreN  42325  dihjatc1  42336  dihmeetlem20N  42351  dih1dimatlem0  42353  dihglblem6  42365  dochexmidlem4  42488  mapdpglem32  42730  mapdh8ad  42804  mapdh9aOLDN  42815  hdmap11lem2  42867  hdmap14lem6  42898  frlmfzowrdb  43536  mzpmfp  43711  mzpsubst  43712  pellex  43795  pellfundex  43846  pellfund14gap  43847  qirropth  43868  rmxypos  43907  congmul  43927  congsub  43930  mzpcong  43932  coprmdvdsb  43945  jm2.15nn0  43963  jm2.16nn0  43964  rpnnen3lem  43991  idomsubgmo  44153  relexp01min  44672  mullimc  46572  islptre  46575  mullimcf  46579  addlimc  46602  0ellimcdiv  46603  limsupre3lem  46686  limsupre3uzlem  46689  fourierdlem48  47108  fourierdlem80  47140  opnvonmbllem2  47587  ovolval5lem3  47608  ovnovollem3  47612  difltmodne  48362  isubgr3stgrlem1  49008  grlimedgclnbgr  49037  mapprop  49402  lincfsuppcl  49469  lindslinindimp2lem3  49516  itsclc0lem1  49812  itsclc0lem2  49813  itschlc0yqe  49816  itsclc0xyqsolr  49825  swapffunc  50334  fucofunc  50411  fucoppc  50462