Theorem simp3r 1203

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

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

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 1088

This theorem is referenced by:  simp13r  1290  simp23r  1296  simp33r  1302  f1oiso2  7286  tfisi  7789  tfrlem5  8299  omeulem1  8497  omeulem2  8498  elfiun  9314  isfin2-2  10210  addlid  11296  mulcan  11754  mulcan2  11755  divass  11794  divdir  11801  div11OLD  11805  ltdiv1  11986  ltmuldiv  11995  lediv2  12012  xaddass2  13149  xlt2add  13159  expaddz  14013  expmulz  14015  resqrex  15157  resqrtcl  15160  o1add  15521  o1mul  15522  o1sub  15523  dvdsgcd  16455  rpexp12i  16635  pythagtriplem4  16731  pythagtriplem11  16737  pythagtriplem13  16739  pcpremul  16755  pceu  16758  pcqmul  16765  pcqdiv  16769  f1ocpbllem  17428  funcoppc  17782  funcres  17803  catcisolem  18017  1stfcl  18103  2ndfcl  18104  prfcl  18109  evlfcl  18128  curf1cl  18134  curfcl  18138  hofcl  18165  latjlej12  18361  latmlem12  18377  latj4  18395  latj4rot  18396  symgsssg  19380  symgfisg  19381  odcong  19462  cmn4  19714  ablsub4  19723  abladdsub4  19724  lsm4  19773  abvdom  20746  abvtrivd  20748  orngmul  20781  lspsolvlem  21080  lbsextlem2  21097  lidlsubcl  21162  frlmbas3  21714  matinvgcell  22351  matmulcell  22361  ma1repveval  22487  mdetunilem3  22530  mdetuni0  22537  mdetmul  22539  hausflimlem  23895  psmetlecl  24231  xmetlecl  24262  prdsxmetlem  24284  xblcntrps  24326  xblcntr  24327  bndth  24885  cph2ass  25141  iscau3  25206  dvres2  25841  coemullem  26183  vieta1  26248  aalioulem4  26271  cxpcn3lem  26685  angcan  26740  divsqrtsumlem  26918  dchrmusumlema  27432  dchrvmasumlema  27439  dchrisum0lema  27453  logdivsum  27472  padicabv  27569  cofcut1  27865  cofcut2  27867  divsmulw  28133  precsexlem8  28153  precsexlem9  28154  ax5seglem3  28910  ax5seglem6  28913  axpasch  28920  axeuclid  28942  axcontlem4  28946  axcontlem8  28950  trlsonistrl  29686  pthonispth  29725  spthonisspth  29729  wspthneq1eq2  29839  frgr2wwlkeqm  30309  adjlnop  32064  xreceu  32900  rhmdvd  33287  measvunilem  34223  measvuni  34225  bnj1128  35000  umgr2cycl  35183  satfv1fvfmla1  35465  cgrcomim  36029  cgrcoml  36036  cgrcomr  36037  cgrdegen  36044  segconeu  36051  btwnintr  36059  btwnexch3  36060  btwnouttr2  36062  btwnouttr  36064  btwnexch  36065  ifscgr  36084  lineext  36116  linecgr  36121  lineid  36123  idinside  36124  btwnconn1lem3  36129  btwnconn1lem4  36130  btwnconn1lem14  36140  btwnconn2  36142  btwnconn3  36143  midofsegid  36144  btwnoutside  36165  outsideoftr  36169  lineunray  36187  lineelsb2  36188  itg2addnclem  37717  cnres2  37809  heibor  37867  lsmcv2  39074  lcvat  39075  lcvexchlem4  39082  lcvexchlem5  39083  lfladd  39111  lflsub  39112  lflmul  39113  lshpkrlem4  39158  latm4  39278  omlmod1i2N  39305  cvlsupr7  39393  cvlsupr8  39394  hlatj4  39419  hlrelat3  39457  cvrval3  39458  atcvrj1  39476  atlelt  39483  2atlt  39484  2atjm  39490  3noncolr2  39494  athgt  39501  3dimlem2  39504  3dimlem4OLDN  39510  1cvratex  39518  ps-1  39522  ps-2  39523  hlatexch3N  39525  llnle  39563  atcvrlln2  39564  atcvrlln  39565  lplni2  39582  lplnle  39585  lplnnle2at  39586  lplnnlelln  39588  llncvrlpln2  39602  2llnmeqat  39616  lvolnle3at  39627  lvolnlelln  39629  4atlem0ae  39639  lneq2at  39823  lnjatN  39825  lncvrat  39827  2lnat  39829  elpaddri  39847  paddasslem2  39866  padd4N  39885  hlmod1i  39901  llnexchb2  39914  dalawlem2  39917  pclfinN  39945  pexmidlem4N  40018  pl42lem1N  40024  lhp2lt  40046  lhpexle1  40053  lhpexle2lem  40054  lhpj1  40067  lhpmcvr5N  40072  lhp2at0  40077  lhp2at0nle  40080  lhple  40087  lhpat  40088  lhpat4N  40089  4atexlemnslpq  40101  4atexlem7  40120  ltrn11  40171  ltrnle  40174  ltrnm  40176  ltrnj  40177  ltrncvr  40178  ltrnel  40184  ltrncnvel  40187  ltrncnv  40191  trlat  40214  trl0  40215  trlnidat  40218  trlnid  40224  ltrnatlw  40228  trlne  40230  trlval4  40233  cdlemc5  40240  cdlemd2  40244  cdlemd7  40249  cdlemd8  40250  cdlemd9  40251  cdleme0c  40258  cdleme0e  40262  cdleme0fN  40263  cdleme3g  40279  cdleme3h  40280  cdleme5  40285  cdleme11c  40306  cdleme11h  40311  cdleme11j  40312  cdleme11k  40313  cdleme0nex  40335  cdleme18a  40336  cdleme22gb  40339  cdleme20zN  40346  cdleme20c  40356  cdleme20k  40364  cdleme21a  40370  cdleme21b  40371  cdleme21c  40372  cdleme21ct  40374  cdleme21h  40379  cdleme22d  40388  cdleme22f  40391  cdleme26ee  40405  cdleme30a  40423  cdlemefs45eN  40476  cdleme36a  40505  cdleme36m  40506  cdleme39a  40510  cdleme42b  40523  cdleme43dN  40537  cdlemeg47rv2  40555  cdlemeg46sfg  40565  cdlemeg46rjgN  40567  cdlemeg46rgv  40573  cdlemeg46req  40574  cdlemeg46gfv  40575  cdleme48d  40580  cdleme50ltrn  40602  cdlemf1  40606  cdlemf  40608  cdlemg2dN  40635  cdlemg2fvlem  40639  cdlemg2l  40648  cdlemg7fvbwN  40652  cdlemg7aN  40670  cdlemg10c  40684  cdlemg17a  40706  cdlemg17dALTN  40709  cdlemg18a  40723  cdlemg18b  40724  cdlemg31b0a  40740  cdlemg31a  40742  cdlemg31b  40743  ltrnco  40764  cdlemg48  40782  tgrpov  40793  tendoco2  40813  tendoplco2  40824  cdlemh1  40860  cdlemk1  40876  cdlemk26b-3  40950  cdlemk27-3  40952  cdlemk28-3  40953  cdlemk34  40955  cdlemkfid1N  40966  cdlemkid3N  40978  cdlemkid4  40979  cdlemk35s-id  40983  cdlemk39s-id  40985  cdlemk51  40998  tendospcanN  41068  cdlemm10N  41163  dicvaddcl  41235  dicvscacl  41236  cdlemn6  41247  dihvalcq2  41292  dihord6b  41305  dihord5apre  41307  dihglbcpreN  41345  dihjatc1  41356  dihmeetlem20N  41371  dih1dimatlem0  41373  dihglblem6  41385  dochexmidlem4  41508  mapdpglem32  41750  mapdh8ad  41824  mapdh9aOLDN  41835  hdmap11lem2  41887  hdmap14lem6  41918  frlmfzowrdb  42543  mzpmfp  42786  mzpsubst  42787  pellex  42874  pellfundex  42925  pellfund14gap  42926  qirropth  42947  rmxypos  42986  congmul  43006  congsub  43009  mzpcong  43011  coprmdvdsb  43024  jm2.15nn0  43042  jm2.16nn0  43043  rpnnen3lem  43070  idomsubgmo  43232  relexp01min  43752  mullimc  45662  islptre  45665  mullimcf  45669  addlimc  45692  0ellimcdiv  45693  limsupre3lem  45776  limsupre3uzlem  45779  fourierdlem48  46198  fourierdlem80  46230  opnvonmbllem2  46677  ovolval5lem3  46698  ovnovollem3  46702  difltmodne  47379  isubgr3stgrlem1  48003  grlimedgclnbgr  48032  mapprop  48383  lincfsuppcl  48451  lindslinindimp2lem3  48498  itsclc0lem1  48794  itsclc0lem2  48795  itschlc0yqe  48798  itsclc0xyqsolr  48807  swapffunc  49320  fucofunc  49397  fucoppc  49448