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  7293  tfisi  7799  tfrlem5  8309  omeulem1  8507  omeulem2  8508  elfiun  9339  isfin2-2  10232  addlid  11317  mulcan  11775  mulcan2  11776  divass  11815  divdir  11822  div11OLD  11826  ltdiv1  12007  ltmuldiv  12016  lediv2  12033  xaddass2  13170  xlt2add  13180  expaddz  14031  expmulz  14033  resqrex  15175  resqrtcl  15178  o1add  15539  o1mul  15540  o1sub  15541  dvdsgcd  16473  rpexp12i  16653  pythagtriplem4  16749  pythagtriplem11  16755  pythagtriplem13  16757  pcpremul  16773  pceu  16776  pcqmul  16783  pcqdiv  16787  f1ocpbllem  17446  funcoppc  17800  funcres  17821  catcisolem  18035  1stfcl  18121  2ndfcl  18122  prfcl  18127  evlfcl  18146  curf1cl  18152  curfcl  18156  hofcl  18183  latjlej12  18379  latmlem12  18395  latj4  18413  latj4rot  18414  symgsssg  19364  symgfisg  19365  odcong  19446  cmn4  19698  ablsub4  19707  abladdsub4  19708  lsm4  19757  abvdom  20733  abvtrivd  20735  orngmul  20768  lspsolvlem  21067  lbsextlem2  21084  lidlsubcl  21149  frlmbas3  21701  matinvgcell  22338  matmulcell  22348  ma1repveval  22474  mdetunilem3  22517  mdetuni0  22524  mdetmul  22526  hausflimlem  23882  psmetlecl  24219  xmetlecl  24250  prdsxmetlem  24272  xblcntrps  24314  xblcntr  24315  bndth  24873  cph2ass  25129  iscau3  25194  dvres2  25829  coemullem  26171  vieta1  26236  aalioulem4  26259  cxpcn3lem  26673  angcan  26728  divsqrtsumlem  26906  dchrmusumlema  27420  dchrvmasumlema  27427  dchrisum0lema  27441  logdivsum  27460  padicabv  27557  cofcut1  27851  cofcut2  27853  divsmulw  28119  precsexlem8  28139  precsexlem9  28140  ax5seglem3  28894  ax5seglem6  28897  axpasch  28904  axeuclid  28926  axcontlem4  28930  axcontlem8  28934  trlsonistrl  29670  pthonispth  29709  spthonisspth  29713  wspthneq1eq2  29823  frgr2wwlkeqm  30293  adjlnop  32048  xreceu  32875  rhmdvd  33275  measvunilem  34181  measvuni  34183  bnj1128  34959  umgr2cycl  35116  satfv1fvfmla1  35398  cgrcomim  35965  cgrcoml  35972  cgrcomr  35973  cgrdegen  35980  segconeu  35987  btwnintr  35995  btwnexch3  35996  btwnouttr2  35998  btwnouttr  36000  btwnexch  36001  ifscgr  36020  lineext  36052  linecgr  36057  lineid  36059  idinside  36060  btwnconn1lem3  36065  btwnconn1lem4  36066  btwnconn1lem14  36076  btwnconn2  36078  btwnconn3  36079  midofsegid  36080  btwnoutside  36101  outsideoftr  36105  lineunray  36123  lineelsb2  36124  itg2addnclem  37653  cnres2  37745  heibor  37803  lsmcv2  39010  lcvat  39011  lcvexchlem4  39018  lcvexchlem5  39019  lfladd  39047  lflsub  39048  lflmul  39049  lshpkrlem4  39094  latm4  39214  omlmod1i2N  39241  cvlsupr7  39329  cvlsupr8  39330  hlatj4  39355  hlrelat3  39394  cvrval3  39395  atcvrj1  39413  atlelt  39420  2atlt  39421  2atjm  39427  3noncolr2  39431  athgt  39438  3dimlem2  39441  3dimlem4OLDN  39447  1cvratex  39455  ps-1  39459  ps-2  39460  hlatexch3N  39462  llnle  39500  atcvrlln2  39501  atcvrlln  39502  lplni2  39519  lplnle  39522  lplnnle2at  39523  lplnnlelln  39525  llncvrlpln2  39539  2llnmeqat  39553  lvolnle3at  39564  lvolnlelln  39566  4atlem0ae  39576  lneq2at  39760  lnjatN  39762  lncvrat  39764  2lnat  39766  elpaddri  39784  paddasslem2  39803  padd4N  39822  hlmod1i  39838  llnexchb2  39851  dalawlem2  39854  pclfinN  39882  pexmidlem4N  39955  pl42lem1N  39961  lhp2lt  39983  lhpexle1  39990  lhpexle2lem  39991  lhpj1  40004  lhpmcvr5N  40009  lhp2at0  40014  lhp2at0nle  40017  lhple  40024  lhpat  40025  lhpat4N  40026  4atexlemnslpq  40038  4atexlem7  40057  ltrn11  40108  ltrnle  40111  ltrnm  40113  ltrnj  40114  ltrncvr  40115  ltrnel  40121  ltrncnvel  40124  ltrncnv  40128  trlat  40151  trl0  40152  trlnidat  40155  trlnid  40161  ltrnatlw  40165  trlne  40167  trlval4  40170  cdlemc5  40177  cdlemd2  40181  cdlemd7  40186  cdlemd8  40187  cdlemd9  40188  cdleme0c  40195  cdleme0e  40199  cdleme0fN  40200  cdleme3g  40216  cdleme3h  40217  cdleme5  40222  cdleme11c  40243  cdleme11h  40248  cdleme11j  40249  cdleme11k  40250  cdleme0nex  40272  cdleme18a  40273  cdleme22gb  40276  cdleme20zN  40283  cdleme20c  40293  cdleme20k  40301  cdleme21a  40307  cdleme21b  40308  cdleme21c  40309  cdleme21ct  40311  cdleme21h  40316  cdleme22d  40325  cdleme22f  40328  cdleme26ee  40342  cdleme30a  40360  cdlemefs45eN  40413  cdleme36a  40442  cdleme36m  40443  cdleme39a  40447  cdleme42b  40460  cdleme43dN  40474  cdlemeg47rv2  40492  cdlemeg46sfg  40502  cdlemeg46rjgN  40504  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemeg46gfv  40512  cdleme48d  40517  cdleme50ltrn  40539  cdlemf1  40543  cdlemf  40545  cdlemg2dN  40572  cdlemg2fvlem  40576  cdlemg2l  40585  cdlemg7fvbwN  40589  cdlemg7aN  40607  cdlemg10c  40621  cdlemg17a  40643  cdlemg17dALTN  40646  cdlemg18a  40660  cdlemg18b  40661  cdlemg31b0a  40677  cdlemg31a  40679  cdlemg31b  40680  ltrnco  40701  cdlemg48  40719  tgrpov  40730  tendoco2  40750  tendoplco2  40761  cdlemh1  40797  cdlemk1  40813  cdlemk26b-3  40887  cdlemk27-3  40889  cdlemk28-3  40890  cdlemk34  40892  cdlemkfid1N  40903  cdlemkid3N  40915  cdlemkid4  40916  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk51  40935  tendospcanN  41005  cdlemm10N  41100  dicvaddcl  41172  dicvscacl  41173  cdlemn6  41184  dihvalcq2  41229  dihord6b  41242  dihord5apre  41244  dihglbcpreN  41282  dihjatc1  41293  dihmeetlem20N  41308  dih1dimatlem0  41310  dihglblem6  41322  dochexmidlem4  41445  mapdpglem32  41687  mapdh8ad  41761  mapdh9aOLDN  41772  hdmap11lem2  41824  hdmap14lem6  41855  frlmfzowrdb  42480  mzpmfp  42723  mzpsubst  42724  pellex  42811  pellfundex  42862  pellfund14gap  42863  qirropth  42884  rmxypos  42923  congmul  42943  congsub  42946  mzpcong  42948  coprmdvdsb  42961  jm2.15nn0  42979  jm2.16nn0  42980  rpnnen3lem  43007  idomsubgmo  43169  relexp01min  43689  mullimc  45601  islptre  45604  mullimcf  45608  addlimc  45633  0ellimcdiv  45634  limsupre3lem  45717  limsupre3uzlem  45720  fourierdlem48  46139  fourierdlem80  46171  opnvonmbllem2  46618  ovolval5lem3  46639  ovnovollem3  46643  difltmodne  47330  isubgr3stgrlem1  47954  grlimedgclnbgr  47983  mapprop  48334  lincfsuppcl  48402  lindslinindimp2lem3  48449  itsclc0lem1  48745  itsclc0lem2  48746  itschlc0yqe  48749  itsclc0xyqsolr  48758  swapffunc  49271  fucofunc  49348  fucoppc  49399