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  7298  tfisi  7801  tfrlem5  8311  omeulem1  8509  omeulem2  8510  elfiun  9333  isfin2-2  10229  addlid  11316  mulcan  11774  mulcan2  11775  divass  11814  divdir  11821  div11OLD  11825  ltdiv1  12006  ltmuldiv  12015  lediv2  12032  xaddass2  13165  xlt2add  13175  expaddz  14029  expmulz  14031  resqrex  15173  resqrtcl  15176  o1add  15537  o1mul  15538  o1sub  15539  dvdsgcd  16471  rpexp12i  16651  pythagtriplem4  16747  pythagtriplem11  16753  pythagtriplem13  16755  pcpremul  16771  pceu  16774  pcqmul  16781  pcqdiv  16785  f1ocpbllem  17445  funcoppc  17799  funcres  17820  catcisolem  18034  1stfcl  18120  2ndfcl  18121  prfcl  18126  evlfcl  18145  curf1cl  18151  curfcl  18155  hofcl  18182  latjlej12  18378  latmlem12  18394  latj4  18412  latj4rot  18413  symgsssg  19396  symgfisg  19397  odcong  19478  cmn4  19730  ablsub4  19739  abladdsub4  19740  lsm4  19789  abvdom  20763  abvtrivd  20765  orngmul  20798  lspsolvlem  21097  lbsextlem2  21114  lidlsubcl  21179  frlmbas3  21731  matinvgcell  22379  matmulcell  22389  ma1repveval  22515  mdetunilem3  22558  mdetuni0  22565  mdetmul  22567  hausflimlem  23923  psmetlecl  24259  xmetlecl  24290  prdsxmetlem  24312  xblcntrps  24354  xblcntr  24355  bndth  24913  cph2ass  25169  iscau3  25234  dvres2  25869  coemullem  26211  vieta1  26276  aalioulem4  26299  cxpcn3lem  26713  angcan  26768  divsqrtsumlem  26946  dchrmusumlema  27460  dchrvmasumlema  27467  dchrisum0lema  27481  logdivsum  27500  padicabv  27597  cofcut1  27916  cofcut2  27918  divmulsw  28189  precsexlem8  28210  precsexlem9  28211  bdayfinbndlem1  28463  ax5seglem3  29004  ax5seglem6  29007  axpasch  29014  axeuclid  29036  axcontlem4  29040  axcontlem8  29044  trlsonistrl  29780  pthonispth  29819  spthonisspth  29823  wspthneq1eq2  29933  frgr2wwlkeqm  30406  adjlnop  32161  xreceu  33003  rhmdvd  33405  measvunilem  34369  measvuni  34371  bnj1128  35146  umgr2cycl  35335  satfv1fvfmla1  35617  cgrcomim  36183  cgrcoml  36190  cgrcomr  36191  cgrdegen  36198  segconeu  36205  btwnintr  36213  btwnexch3  36214  btwnouttr2  36216  btwnouttr  36218  btwnexch  36219  ifscgr  36238  lineext  36270  linecgr  36275  lineid  36277  idinside  36278  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem14  36294  btwnconn2  36296  btwnconn3  36297  midofsegid  36298  btwnoutside  36319  outsideoftr  36323  lineunray  36341  lineelsb2  36342  itg2addnclem  37872  cnres2  37964  heibor  38022  lsmcv2  39289  lcvat  39290  lcvexchlem4  39297  lcvexchlem5  39298  lfladd  39326  lflsub  39327  lflmul  39328  lshpkrlem4  39373  latm4  39493  omlmod1i2N  39520  cvlsupr7  39608  cvlsupr8  39609  hlatj4  39634  hlrelat3  39672  cvrval3  39673  atcvrj1  39691  atlelt  39698  2atlt  39699  2atjm  39705  3noncolr2  39709  athgt  39716  3dimlem2  39719  3dimlem4OLDN  39725  1cvratex  39733  ps-1  39737  ps-2  39738  hlatexch3N  39740  llnle  39778  atcvrlln2  39779  atcvrlln  39780  lplni2  39797  lplnle  39800  lplnnle2at  39801  lplnnlelln  39803  llncvrlpln2  39817  2llnmeqat  39831  lvolnle3at  39842  lvolnlelln  39844  4atlem0ae  39854  lneq2at  40038  lnjatN  40040  lncvrat  40042  2lnat  40044  elpaddri  40062  paddasslem2  40081  padd4N  40100  hlmod1i  40116  llnexchb2  40129  dalawlem2  40132  pclfinN  40160  pexmidlem4N  40233  pl42lem1N  40239  lhp2lt  40261  lhpexle1  40268  lhpexle2lem  40269  lhpj1  40282  lhpmcvr5N  40287  lhp2at0  40292  lhp2at0nle  40295  lhple  40302  lhpat  40303  lhpat4N  40304  4atexlemnslpq  40316  4atexlem7  40335  ltrn11  40386  ltrnle  40389  ltrnm  40391  ltrnj  40392  ltrncvr  40393  ltrnel  40399  ltrncnvel  40402  ltrncnv  40406  trlat  40429  trl0  40430  trlnidat  40433  trlnid  40439  ltrnatlw  40443  trlne  40445  trlval4  40448  cdlemc5  40455  cdlemd2  40459  cdlemd7  40464  cdlemd8  40465  cdlemd9  40466  cdleme0c  40473  cdleme0e  40477  cdleme0fN  40478  cdleme3g  40494  cdleme3h  40495  cdleme5  40500  cdleme11c  40521  cdleme11h  40526  cdleme11j  40527  cdleme11k  40528  cdleme0nex  40550  cdleme18a  40551  cdleme22gb  40554  cdleme20zN  40561  cdleme20c  40571  cdleme20k  40579  cdleme21a  40585  cdleme21b  40586  cdleme21c  40587  cdleme21ct  40589  cdleme21h  40594  cdleme22d  40603  cdleme22f  40606  cdleme26ee  40620  cdleme30a  40638  cdlemefs45eN  40691  cdleme36a  40720  cdleme36m  40721  cdleme39a  40725  cdleme42b  40738  cdleme43dN  40752  cdlemeg47rv2  40770  cdlemeg46sfg  40780  cdlemeg46rjgN  40782  cdlemeg46rgv  40788  cdlemeg46req  40789  cdlemeg46gfv  40790  cdleme48d  40795  cdleme50ltrn  40817  cdlemf1  40821  cdlemf  40823  cdlemg2dN  40850  cdlemg2fvlem  40854  cdlemg2l  40863  cdlemg7fvbwN  40867  cdlemg7aN  40885  cdlemg10c  40899  cdlemg17a  40921  cdlemg17dALTN  40924  cdlemg18a  40938  cdlemg18b  40939  cdlemg31b0a  40955  cdlemg31a  40957  cdlemg31b  40958  ltrnco  40979  cdlemg48  40997  tgrpov  41008  tendoco2  41028  tendoplco2  41039  cdlemh1  41075  cdlemk1  41091  cdlemk26b-3  41165  cdlemk27-3  41167  cdlemk28-3  41168  cdlemk34  41170  cdlemkfid1N  41181  cdlemkid3N  41193  cdlemkid4  41194  cdlemk35s-id  41198  cdlemk39s-id  41200  cdlemk51  41213  tendospcanN  41283  cdlemm10N  41378  dicvaddcl  41450  dicvscacl  41451  cdlemn6  41462  dihvalcq2  41507  dihord6b  41520  dihord5apre  41522  dihglbcpreN  41560  dihjatc1  41571  dihmeetlem20N  41586  dih1dimatlem0  41588  dihglblem6  41600  dochexmidlem4  41723  mapdpglem32  41965  mapdh8ad  42039  mapdh9aOLDN  42050  hdmap11lem2  42102  hdmap14lem6  42133  frlmfzowrdb  42759  mzpmfp  42989  mzpsubst  42990  pellex  43077  pellfundex  43128  pellfund14gap  43129  qirropth  43150  rmxypos  43189  congmul  43209  congsub  43212  mzpcong  43214  coprmdvdsb  43227  jm2.15nn0  43245  jm2.16nn0  43246  rpnnen3lem  43273  idomsubgmo  43435  relexp01min  43954  mullimc  45862  islptre  45865  mullimcf  45869  addlimc  45892  0ellimcdiv  45893  limsupre3lem  45976  limsupre3uzlem  45979  fourierdlem48  46398  fourierdlem80  46430  opnvonmbllem2  46877  ovolval5lem3  46898  ovnovollem3  46902  difltmodne  47588  isubgr3stgrlem1  48212  grlimedgclnbgr  48241  mapprop  48592  lincfsuppcl  48659  lindslinindimp2lem3  48706  itsclc0lem1  49002  itsclc0lem2  49003  itschlc0yqe  49006  itsclc0xyqsolr  49015  swapffunc  49527  fucofunc  49604  fucoppc  49655