Theorem simp3r 1083

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl3r  1110  simpr3r  1116  simp13r  1170  simp23r  1176  simp33r  1182  f1oiso2  6502  tfisi  6950  tfrlem5  7363  omeulem1  7549  omeulem2  7550  elfiun  8219  isfin2-2  9024  addid2  10098  mulcan  10543  mulcan2  10544  divass  10582  divdir  10589  div11  10592  ltdiv1  10766  ltmuldiv  10775  lediv2  10792  xaddass2  11952  xlt2add  11962  expaddz  12766  expmulz  12768  resqrex  13839  resqrtcl  13842  o1add  14192  o1mul  14193  o1sub  14194  dvdsgcd  15099  rpexp12i  15272  pythagtriplem4  15362  pythagtriplem11  15368  pythagtriplem13  15370  pcpremul  15386  pceu  15389  pcqmul  15396  pcqdiv  15400  f1ocpbllem  16007  funcoppc  16358  funcres  16379  catcisolem  16579  1stfcl  16660  2ndfcl  16661  prfcl  16666  evlfcl  16685  curf1cl  16691  curfcl  16695  hofcl  16722  latjlej12  16890  latmlem12  16906  latj4  16924  latj4rot  16925  symgsssg  17710  symgfisg  17711  odcong  17791  cmn4  18035  ablsub4  18041  abladdsub4  18042  lsm4  18086  abvdom  18661  abvtrivd  18663  lspsolvlem  18963  lbsextlem2  18980  lidlsubcl  19037  frlmbas3  19934  matinvgcell  20060  matmulcell  20070  ma1repveval  20196  mdetunilem3  20239  mdetuni0  20246  mdetmul  20248  hausflimlem  21593  psmetlecl  21930  xmetlecl  21961  prdsxmetlem  21983  xblcntrps  22025  xblcntr  22026  bndth  22565  cph2ass  22821  iscau3  22884  dvres2  23482  coemullem  23810  vieta1  23871  aalioulem4  23894  cxpcn3lem  24288  angcan  24332  divsqrtsumlem  24506  dchrmusumlema  24982  dchrvmasumlema  24989  dchrisum0lema  25003  logdivsum  25022  padicabv  25119  ax5seglem3  25611  ax5seglem6  25614  axpasch  25621  axeuclid  25643  axcontlem4  25647  axcontlem8  25651  adjlnop  28329  xreceu  28961  orngmul  29134  rhmdvd  29152  measvunilem  29602  measvuni  29604  bnj1128  30312  cgrcomim  31266  cgrcoml  31273  cgrcomr  31274  cgrdegen  31281  segconeu  31288  btwnintr  31296  btwnexch3  31297  btwnouttr2  31299  btwnouttr  31301  btwnexch  31302  ifscgr  31321  lineext  31353  linecgr  31358  lineid  31360  idinside  31361  btwnconn1lem3  31366  btwnconn1lem4  31367  btwnconn1lem14  31377  btwnconn2  31379  btwnconn3  31380  midofsegid  31381  btwnoutside  31402  outsideoftr  31406  lineunray  31424  lineelsb2  31425  itg2addnclem  32631  cnres2  32732  heibor  32790  lsmcv2  33334  lcvat  33335  lcvexchlem4  33342  lcvexchlem5  33343  lfladd  33371  lflsub  33372  lflmul  33373  lshpkrlem4  33418  latm4  33538  omlmod1i2N  33565  cvlsupr7  33653  cvlsupr8  33654  hlatj4  33678  hlrelat3  33716  cvrval3  33717  atcvrj1  33735  atlelt  33742  2atlt  33743  2atjm  33749  3noncolr2  33753  athgt  33760  3dimlem2  33763  3dimlem4OLDN  33769  1cvratex  33777  ps-1  33781  ps-2  33782  hlatexch3N  33784  llnle  33822  atcvrlln2  33823  atcvrlln  33824  lplni2  33841  lplnle  33844  lplnnle2at  33845  lplnnlelln  33847  llncvrlpln2  33861  2llnmeqat  33875  lvolnle3at  33886  lvolnlelln  33888  4atlem0ae  33898  lneq2at  34082  lnjatN  34084  lncvrat  34086  2lnat  34088  elpaddri  34106  paddasslem2  34125  padd4N  34144  hlmod1i  34160  llnexchb2  34173  dalawlem2  34176  pclfinN  34204  pexmidlem4N  34277  pl42lem1N  34283  lhp2lt  34305  lhpexle1  34312  lhpexle2lem  34313  lhpj1  34326  lhpmcvr5N  34331  lhp2at0  34336  lhp2at0nle  34339  lhple  34346  lhpat  34347  lhpat4N  34348  4atexlemnslpq  34360  4atexlem7  34379  ltrn11  34430  ltrnle  34433  ltrnm  34435  ltrnj  34436  ltrncvr  34437  ltrnel  34443  ltrncnvel  34446  ltrncnv  34450  ltrnmwOLD  34456  trlat  34474  trl0  34475  trlnidat  34478  trlnid  34484  ltrnatlw  34488  trlne  34490  trlval4  34493  cdlemc5  34500  cdlemd2  34504  cdlemd7  34509  cdlemd8  34510  cdlemd9  34511  cdleme0c  34518  cdleme0e  34522  cdleme0fN  34523  cdleme3g  34539  cdleme3h  34540  cdleme5  34545  cdleme11c  34566  cdleme11h  34571  cdleme11j  34572  cdleme11k  34573  cdleme0nex  34595  cdleme18a  34596  cdleme22gb  34599  cdleme20zN  34606  cdleme20yOLD  34608  cdleme20c  34617  cdleme20k  34625  cdleme21a  34631  cdleme21b  34632  cdleme21c  34633  cdleme21ct  34635  cdleme21h  34640  cdleme22d  34649  cdleme22f  34652  cdleme26ee  34666  cdleme30a  34684  cdlemefs45eN  34737  cdleme36a  34766  cdleme36m  34767  cdleme39a  34771  cdleme42b  34784  cdleme43dN  34798  cdlemeg47rv2  34816  cdlemeg46sfg  34826  cdlemeg46rjgN  34828  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemeg46gfv  34836  cdleme48d  34841  cdleme50ltrn  34863  cdlemf1  34867  cdlemf  34869  cdlemg2dN  34896  cdlemg2fvlem  34900  cdlemg2l  34909  cdlemg7fvbwN  34913  cdlemg7aN  34931  cdlemg10c  34945  cdlemg17a  34967  cdlemg17dALTN  34970  cdlemg18a  34984  cdlemg18b  34985  cdlemg31b0a  35001  cdlemg31a  35003  cdlemg31b  35004  ltrnco  35025  cdlemg48  35043  tgrpov  35054  tendoco2  35074  tendoplco2  35085  cdlemh1  35121  cdlemk1  35137  cdlemk26b-3  35211  cdlemk27-3  35213  cdlemk28-3  35214  cdlemk34  35216  cdlemkfid1N  35227  cdlemkid3N  35239  cdlemkid4  35240  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk51  35259  tendospcanN  35330  cdlemm10N  35425  dicvaddcl  35497  dicvscacl  35498  cdlemn6  35509  dihvalcq2  35554  dihord6b  35567  dihord5apre  35569  dihglbcpreN  35607  dihjatc1  35618  dihmeetlem20N  35633  dih1dimatlem0  35635  dihglblem6  35647  dochexmidlem4  35770  mapdpglem32  36012  mapdh8ad  36086  mapdh9aOLDN  36098  hdmap11lem2  36152  hdmap14lem6  36183  mzpmfp  36328  mzpsubst  36329  pellex  36417  pellfundex  36468  pellfund14gap  36469  qirropth  36491  rmxypos  36532  congmul  36552  congsub  36555  mzpcong  36557  coprmdvdsb  36570  jm2.15nn0  36588  jm2.16nn0  36589  rpnnen3lem  36616  idomsubgmo  36795  relexp01min  37024  mullimc  38683  islptre  38686  mullimcf  38690  addlimc  38715  0ellimcdiv  38716  fourierdlem48  39047  fourierdlem80  39079  opnvonmbllem2  39523  ovolval5lem3  39544  ovnovollem3  39548  trlsonistrl  40916  pthonispth-av  40952  spthonisspth-av  40956  wspthneq1eq2  41056  lincfsuppcl  41996  lindslinindimp2lem3  42043