Theorem simp3r 1200

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 1133	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp13r  1287  simp23r  1293  simp33r  1299  f1oiso2  7203  tfisi  7680  tfrlem5  8182  omeulem1  8375  omeulem2  8376  elfiun  9119  isfin2-2  10006  addid2  11088  mulcan  11542  mulcan2  11543  divass  11581  divdir  11588  div11  11591  ltdiv1  11769  ltmuldiv  11778  lediv2  11795  xaddass2  12913  xlt2add  12923  expaddz  13755  expmulz  13757  resqrex  14890  resqrtcl  14893  o1add  15251  o1mul  15252  o1sub  15253  dvdsgcd  16180  rpexp12i  16357  pythagtriplem4  16448  pythagtriplem11  16454  pythagtriplem13  16456  pcpremul  16472  pceu  16475  pcqmul  16482  pcqdiv  16486  f1ocpbllem  17152  funcoppc  17506  funcres  17527  catcisolem  17741  1stfcl  17830  2ndfcl  17831  prfcl  17836  evlfcl  17856  curf1cl  17862  curfcl  17866  hofcl  17893  latjlej12  18088  latmlem12  18104  latj4  18122  latj4rot  18123  symgsssg  18990  symgfisg  18991  odcong  19072  cmn4  19321  ablsub4  19329  abladdsub4  19330  lsm4  19376  abvdom  20013  abvtrivd  20015  lspsolvlem  20319  lbsextlem2  20336  lidlsubcl  20400  frlmbas3  20893  matinvgcell  21492  matmulcell  21502  ma1repveval  21628  mdetunilem3  21671  mdetuni0  21678  mdetmul  21680  hausflimlem  23038  psmetlecl  23376  xmetlecl  23407  prdsxmetlem  23429  xblcntrps  23471  xblcntr  23472  bndth  24027  cph2ass  24282  iscau3  24347  dvres2  24981  coemullem  25316  vieta1  25377  aalioulem4  25400  cxpcn3lem  25805  angcan  25857  divsqrtsumlem  26034  dchrmusumlema  26546  dchrvmasumlema  26553  dchrisum0lema  26567  logdivsum  26586  padicabv  26683  ax5seglem3  27202  ax5seglem6  27205  axpasch  27212  axeuclid  27234  axcontlem4  27238  axcontlem8  27242  trlsonistrl  27978  pthonispth  28015  spthonisspth  28019  wspthneq1eq2  28126  frgr2wwlkeqm  28596  adjlnop  30349  xreceu  31098  orngmul  31404  rhmdvd  31422  measvunilem  32080  measvuni  32082  bnj1128  32870  umgr2cycl  33003  satfv1fvfmla1  33285  cofcut1  34017  cofcut2  34018  cgrcomim  34218  cgrcoml  34225  cgrcomr  34226  cgrdegen  34233  segconeu  34240  btwnintr  34248  btwnexch3  34249  btwnouttr2  34251  btwnouttr  34253  btwnexch  34254  ifscgr  34273  lineext  34305  linecgr  34310  lineid  34312  idinside  34313  btwnconn1lem3  34318  btwnconn1lem4  34319  btwnconn1lem14  34329  btwnconn2  34331  btwnconn3  34332  midofsegid  34333  btwnoutside  34354  outsideoftr  34358  lineunray  34376  lineelsb2  34377  itg2addnclem  35755  cnres2  35848  heibor  35906  lsmcv2  36970  lcvat  36971  lcvexchlem4  36978  lcvexchlem5  36979  lfladd  37007  lflsub  37008  lflmul  37009  lshpkrlem4  37054  latm4  37174  omlmod1i2N  37201  cvlsupr7  37289  cvlsupr8  37290  hlatj4  37315  hlrelat3  37353  cvrval3  37354  atcvrj1  37372  atlelt  37379  2atlt  37380  2atjm  37386  3noncolr2  37390  athgt  37397  3dimlem2  37400  3dimlem4OLDN  37406  1cvratex  37414  ps-1  37418  ps-2  37419  hlatexch3N  37421  llnle  37459  atcvrlln2  37460  atcvrlln  37461  lplni2  37478  lplnle  37481  lplnnle2at  37482  lplnnlelln  37484  llncvrlpln2  37498  2llnmeqat  37512  lvolnle3at  37523  lvolnlelln  37525  4atlem0ae  37535  lneq2at  37719  lnjatN  37721  lncvrat  37723  2lnat  37725  elpaddri  37743  paddasslem2  37762  padd4N  37781  hlmod1i  37797  llnexchb2  37810  dalawlem2  37813  pclfinN  37841  pexmidlem4N  37914  pl42lem1N  37920  lhp2lt  37942  lhpexle1  37949  lhpexle2lem  37950  lhpj1  37963  lhpmcvr5N  37968  lhp2at0  37973  lhp2at0nle  37976  lhple  37983  lhpat  37984  lhpat4N  37985  4atexlemnslpq  37997  4atexlem7  38016  ltrn11  38067  ltrnle  38070  ltrnm  38072  ltrnj  38073  ltrncvr  38074  ltrnel  38080  ltrncnvel  38083  ltrncnv  38087  trlat  38110  trl0  38111  trlnidat  38114  trlnid  38120  ltrnatlw  38124  trlne  38126  trlval4  38129  cdlemc5  38136  cdlemd2  38140  cdlemd7  38145  cdlemd8  38146  cdlemd9  38147  cdleme0c  38154  cdleme0e  38158  cdleme0fN  38159  cdleme3g  38175  cdleme3h  38176  cdleme5  38181  cdleme11c  38202  cdleme11h  38207  cdleme11j  38208  cdleme11k  38209  cdleme0nex  38231  cdleme18a  38232  cdleme22gb  38235  cdleme20zN  38242  cdleme20c  38252  cdleme20k  38260  cdleme21a  38266  cdleme21b  38267  cdleme21c  38268  cdleme21ct  38270  cdleme21h  38275  cdleme22d  38284  cdleme22f  38287  cdleme26ee  38301  cdleme30a  38319  cdlemefs45eN  38372  cdleme36a  38401  cdleme36m  38402  cdleme39a  38406  cdleme42b  38419  cdleme43dN  38433  cdlemeg47rv2  38451  cdlemeg46sfg  38461  cdlemeg46rjgN  38463  cdlemeg46rgv  38469  cdlemeg46req  38470  cdlemeg46gfv  38471  cdleme48d  38476  cdleme50ltrn  38498  cdlemf1  38502  cdlemf  38504  cdlemg2dN  38531  cdlemg2fvlem  38535  cdlemg2l  38544  cdlemg7fvbwN  38548  cdlemg7aN  38566  cdlemg10c  38580  cdlemg17a  38602  cdlemg17dALTN  38605  cdlemg18a  38619  cdlemg18b  38620  cdlemg31b0a  38636  cdlemg31a  38638  cdlemg31b  38639  ltrnco  38660  cdlemg48  38678  tgrpov  38689  tendoco2  38709  tendoplco2  38720  cdlemh1  38756  cdlemk1  38772  cdlemk26b-3  38846  cdlemk27-3  38848  cdlemk28-3  38849  cdlemk34  38851  cdlemkfid1N  38862  cdlemkid3N  38874  cdlemkid4  38875  cdlemk35s-id  38879  cdlemk39s-id  38881  cdlemk51  38894  tendospcanN  38964  cdlemm10N  39059  dicvaddcl  39131  dicvscacl  39132  cdlemn6  39143  dihvalcq2  39188  dihord6b  39201  dihord5apre  39203  dihglbcpreN  39241  dihjatc1  39252  dihmeetlem20N  39267  dih1dimatlem0  39269  dihglblem6  39281  dochexmidlem4  39404  mapdpglem32  39646  mapdh8ad  39720  mapdh9aOLDN  39731  hdmap11lem2  39783  hdmap14lem6  39814  frlmfzowrdb  40161  mzpmfp  40485  mzpsubst  40486  pellex  40573  pellfundex  40624  pellfund14gap  40625  qirropth  40646  rmxypos  40685  congmul  40705  congsub  40708  mzpcong  40710  coprmdvdsb  40723  jm2.15nn0  40741  jm2.16nn0  40742  rpnnen3lem  40769  idomsubgmo  40939  relexp01min  41210  mullimc  43047  islptre  43050  mullimcf  43054  addlimc  43079  0ellimcdiv  43080  limsupre3lem  43163  limsupre3uzlem  43166  fourierdlem48  43585  fourierdlem80  43617  opnvonmbllem2  44061  ovolval5lem3  44082  ovnovollem3  44086  mapprop  45570  lincfsuppcl  45642  lindslinindimp2lem3  45689  itsclc0lem1  45990  itsclc0lem2  45991  itschlc0yqe  45994  itsclc0xyqsolr  46003