Theorem simp3r 1199

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simp13r  1286  simp23r  1292  simp33r  1298  f1oiso2  7084  tfisi  7553  tfrlem5  7999  omeulem1  8191  omeulem2  8192  elfiun  8878  isfin2-2  9730  addid2  10812  mulcan  11266  mulcan2  11267  divass  11305  divdir  11312  div11  11315  ltdiv1  11493  ltmuldiv  11502  lediv2  11519  xaddass2  12631  xlt2add  12641  expaddz  13469  expmulz  13471  resqrex  14602  resqrtcl  14605  o1add  14962  o1mul  14963  o1sub  14964  dvdsgcd  15882  rpexp12i  16056  pythagtriplem4  16146  pythagtriplem11  16152  pythagtriplem13  16154  pcpremul  16170  pceu  16173  pcqmul  16180  pcqdiv  16184  f1ocpbllem  16789  funcoppc  17137  funcres  17158  catcisolem  17358  1stfcl  17439  2ndfcl  17440  prfcl  17445  evlfcl  17464  curf1cl  17470  curfcl  17474  hofcl  17501  latjlej12  17669  latmlem12  17685  latj4  17703  latj4rot  17704  symgsssg  18587  symgfisg  18588  odcong  18669  cmn4  18918  ablsub4  18926  abladdsub4  18927  lsm4  18973  abvdom  19602  abvtrivd  19604  lspsolvlem  19907  lbsextlem2  19924  lidlsubcl  19982  frlmbas3  20465  matinvgcell  21040  matmulcell  21050  ma1repveval  21176  mdetunilem3  21219  mdetuni0  21226  mdetmul  21228  hausflimlem  22584  psmetlecl  22922  xmetlecl  22953  prdsxmetlem  22975  xblcntrps  23017  xblcntr  23018  bndth  23563  cph2ass  23818  iscau3  23882  dvres2  24515  coemullem  24847  vieta1  24908  aalioulem4  24931  cxpcn3lem  25336  angcan  25388  divsqrtsumlem  25565  dchrmusumlema  26077  dchrvmasumlema  26084  dchrisum0lema  26098  logdivsum  26117  padicabv  26214  ax5seglem3  26725  ax5seglem6  26728  axpasch  26735  axeuclid  26757  axcontlem4  26761  axcontlem8  26765  trlsonistrl  27498  pthonispth  27535  spthonisspth  27539  wspthneq1eq2  27646  frgr2wwlkeqm  28116  adjlnop  29869  xreceu  30624  orngmul  30927  rhmdvd  30945  measvunilem  31581  measvuni  31583  bnj1128  32372  umgr2cycl  32501  satfv1fvfmla1  32783  cgrcomim  33563  cgrcoml  33570  cgrcomr  33571  cgrdegen  33578  segconeu  33585  btwnintr  33593  btwnexch3  33594  btwnouttr2  33596  btwnouttr  33598  btwnexch  33599  ifscgr  33618  lineext  33650  linecgr  33655  lineid  33657  idinside  33658  btwnconn1lem3  33663  btwnconn1lem4  33664  btwnconn1lem14  33674  btwnconn2  33676  btwnconn3  33677  midofsegid  33678  btwnoutside  33699  outsideoftr  33703  lineunray  33721  lineelsb2  33722  itg2addnclem  35108  cnres2  35201  heibor  35259  lsmcv2  36325  lcvat  36326  lcvexchlem4  36333  lcvexchlem5  36334  lfladd  36362  lflsub  36363  lflmul  36364  lshpkrlem4  36409  latm4  36529  omlmod1i2N  36556  cvlsupr7  36644  cvlsupr8  36645  hlatj4  36670  hlrelat3  36708  cvrval3  36709  atcvrj1  36727  atlelt  36734  2atlt  36735  2atjm  36741  3noncolr2  36745  athgt  36752  3dimlem2  36755  3dimlem4OLDN  36761  1cvratex  36769  ps-1  36773  ps-2  36774  hlatexch3N  36776  llnle  36814  atcvrlln2  36815  atcvrlln  36816  lplni2  36833  lplnle  36836  lplnnle2at  36837  lplnnlelln  36839  llncvrlpln2  36853  2llnmeqat  36867  lvolnle3at  36878  lvolnlelln  36880  4atlem0ae  36890  lneq2at  37074  lnjatN  37076  lncvrat  37078  2lnat  37080  elpaddri  37098  paddasslem2  37117  padd4N  37136  hlmod1i  37152  llnexchb2  37165  dalawlem2  37168  pclfinN  37196  pexmidlem4N  37269  pl42lem1N  37275  lhp2lt  37297  lhpexle1  37304  lhpexle2lem  37305  lhpj1  37318  lhpmcvr5N  37323  lhp2at0  37328  lhp2at0nle  37331  lhple  37338  lhpat  37339  lhpat4N  37340  4atexlemnslpq  37352  4atexlem7  37371  ltrn11  37422  ltrnle  37425  ltrnm  37427  ltrnj  37428  ltrncvr  37429  ltrnel  37435  ltrncnvel  37438  ltrncnv  37442  trlat  37465  trl0  37466  trlnidat  37469  trlnid  37475  ltrnatlw  37479  trlne  37481  trlval4  37484  cdlemc5  37491  cdlemd2  37495  cdlemd7  37500  cdlemd8  37501  cdlemd9  37502  cdleme0c  37509  cdleme0e  37513  cdleme0fN  37514  cdleme3g  37530  cdleme3h  37531  cdleme5  37536  cdleme11c  37557  cdleme11h  37562  cdleme11j  37563  cdleme11k  37564  cdleme0nex  37586  cdleme18a  37587  cdleme22gb  37590  cdleme20zN  37597  cdleme20c  37607  cdleme20k  37615  cdleme21a  37621  cdleme21b  37622  cdleme21c  37623  cdleme21ct  37625  cdleme21h  37630  cdleme22d  37639  cdleme22f  37642  cdleme26ee  37656  cdleme30a  37674  cdlemefs45eN  37727  cdleme36a  37756  cdleme36m  37757  cdleme39a  37761  cdleme42b  37774  cdleme43dN  37788  cdlemeg47rv2  37806  cdlemeg46sfg  37816  cdlemeg46rjgN  37818  cdlemeg46rgv  37824  cdlemeg46req  37825  cdlemeg46gfv  37826  cdleme48d  37831  cdleme50ltrn  37853  cdlemf1  37857  cdlemf  37859  cdlemg2dN  37886  cdlemg2fvlem  37890  cdlemg2l  37899  cdlemg7fvbwN  37903  cdlemg7aN  37921  cdlemg10c  37935  cdlemg17a  37957  cdlemg17dALTN  37960  cdlemg18a  37974  cdlemg18b  37975  cdlemg31b0a  37991  cdlemg31a  37993  cdlemg31b  37994  ltrnco  38015  cdlemg48  38033  tgrpov  38044  tendoco2  38064  tendoplco2  38075  cdlemh1  38111  cdlemk1  38127  cdlemk26b-3  38201  cdlemk27-3  38203  cdlemk28-3  38204  cdlemk34  38206  cdlemkfid1N  38217  cdlemkid3N  38229  cdlemkid4  38230  cdlemk35s-id  38234  cdlemk39s-id  38236  cdlemk51  38249  tendospcanN  38319  cdlemm10N  38414  dicvaddcl  38486  dicvscacl  38487  cdlemn6  38498  dihvalcq2  38543  dihord6b  38556  dihord5apre  38558  dihglbcpreN  38596  dihjatc1  38607  dihmeetlem20N  38622  dih1dimatlem0  38624  dihglblem6  38636  dochexmidlem4  38759  mapdpglem32  39001  mapdh8ad  39075  mapdh9aOLDN  39086  hdmap11lem2  39138  hdmap14lem6  39169  frlmfzowrdb  39438  mzpmfp  39688  mzpsubst  39689  pellex  39776  pellfundex  39827  pellfund14gap  39828  qirropth  39849  rmxypos  39888  congmul  39908  congsub  39911  mzpcong  39913  coprmdvdsb  39926  jm2.15nn0  39944  jm2.16nn0  39945  rpnnen3lem  39972  idomsubgmo  40142  relexp01min  40414  mullimc  42258  islptre  42261  mullimcf  42265  addlimc  42290  0ellimcdiv  42291  limsupre3lem  42374  limsupre3uzlem  42377  fourierdlem48  42796  fourierdlem80  42828  opnvonmbllem2  43272  ovolval5lem3  43293  ovnovollem3  43297  mapprop  44748  lincfsuppcl  44822  lindslinindimp2lem3  44869  itsclc0lem1  45170  itsclc0lem2  45171  itschlc0yqe  45174  itsclc0xyqsolr  45183